Axioms for the theory of proveit.linear_algebra.linear_maps

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.

from proveit import Function, Lambda, Conditional, Composition
from proveit import c, x, y, A, B, K, P, V, W, Px, Py
from proveit.logic import And, Iff, Forall, Equals, InSet
from proveit.linear_algebra import (
    VecSpaces, LinMap, VecAdd, vec_subtract, ScalarMult, VecZero, Identity, Commutator, AntiCommutator)

%begin axioms

Defining axioms for theory 'proveit.linear_algebra.linear_maps'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

A linear map is a map with linear properties

lin_map_def = Forall(
    K, Forall(
        (V, W), Forall(
            P, Iff(InSet(P, LinMap(V, W)),
                   And(Forall(x, InSet(Px, W), domain=V),
                       Forall((x, y), Equals(Function(P, VecAdd(x, y)),
                                             VecAdd(Px, Py)),
                              domain=V),
                       Forall(c, Forall(x, Equals(Function(P, ScalarMult(c, x)),
                                                  ScalarMult(c, Px)),
                                        domain=V),
                              domain=K)).with_wrapping_at(2, 4)).with_wrap_after_operator()),
        domain=VecSpaces(K)))

lin_map_def:

A linear map is, itself, a vector space

by defining vector addition and scalar addition on a linear map in the following manner.

vec_add_lin_map = Forall(
    K, Forall(
        (V, W), Forall(
            (A, B), Equals(VecAdd(A, B),
                           Lambda(x, Conditional(
                               VecAdd(Function(A, x), 
                                      Function(B, x)),
                               InSet(x, V)))),
            domain=LinMap(V, W)),
        domain=VecSpaces(K)))

vec_add_lin_map:

scalar_mult_lin_map = Forall(
    K, Forall(
        (V, W), Forall(
            c, Forall(
                P, Equals(ScalarMult(c, P),
                          Lambda(x, Conditional(ScalarMult(c, Function(P, x)),
                                                InSet(x, V)))),
                domain=LinMap(V, W)),
            domain=K),
        domain=VecSpaces(K)))

scalar_mult_lin_map:

identity_def = Forall(V, Equals(Identity(V), Lambda(x, Conditional(x, InSet(x, V)))))

identity_def:

Commutator and Anti-commutator

commutator_def = Forall(
    K, Forall(
        V, Forall((A, B), Equals(Commutator(A, B), vec_subtract(Composition(A, B), Composition(B, A))),
                  domain=V),
        domain=VecSpaces(K)))

commutator_def:

anti_commutator_def = Forall(
    K, Forall(
        V, Forall((A, B), Equals(AntiCommutator(A, B), VecAdd(Composition(A, B), Composition(B, A))),
                  domain=V),
        domain=VecSpaces(K)))

anti_commutator_def:

%end axioms

These axioms may now be imported from the theory package: proveit.linear_algebra.linear_maps