HomeHome Metamath Proof Explorer
Theorem List (p. 353 of 402) 		< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26569) 		  Hilbert Space Explorer  Hilbert Space Explorer
(26570-28092) 		  Users' Mathboxes  Users' Mathboxes
(28093-40161) 		 

Theorem List for Metamath Proof Explorer - 35201-35300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmapdlsm 35201 Subspace sum is preserved by the map defined by df-mapd 35162. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- S = ( LSubSp ` U )   &    |- .(+) = ( LSSum ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( LSSum ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( M ` ( X .(+) Y ) ) = ( ( M ` X ) .+b ( M ` Y ) ) )
 
Theoremmapd0 35202 Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- O = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .0. = ( 0g ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( M ` { O } ) = { .0. } )
 
TheoremmapdcnvatN 35203 Atoms are preserved by the map defined by df-mapd 35162. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- B = (LSAtoms ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. B )   =>    |- ( ph -> ( `' M ` Q ) e. A )
 
Theoremmapdat 35204 Atoms are preserved by the map defined by df-mapd 35162. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- A = (LSAtoms ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- B = (LSAtoms ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( M ` Q ) e. B )
 
Theoremmapdspex 35205* The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- B = ( Base ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )
 
Theoremmapdn0 35206 Transfer non-zero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- .0. = ( 0g ` U )   &    |- Z = ( 0g ` C )   &    |- ( ph -> X e. ( V \ { .0. } ) )   =>    |- ( ph -> F e. ( D \ { Z } ) )
 
Theoremmapdncol 35207 Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( J ` { F } ) =/= ( J ` { G } ) )
 
Theoremmapdindp 35208 Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )   &    |- ( ph -> Z e. V )   &    |- ( ph -> E e. D )   &    |- ( ph -> ( M ` ( N ` { Z } ) ) = ( J ` { E } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   =>    |- ( ph -> -. F e. ( J ` { G , E } ) )
 
Theoremmapdpglem1 35209 Lemma for mapdpg 35243. Baer p. 44, last line: "(F(x-y))* =< (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   =>    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) C_ ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
 
Theoremmapdpglem2 35210* Lemma for mapdpg 35243. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d t ph locally to avoid clashes with later substitutions into ph.) (Contributed by NM, 15-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   =>    |- ( ph -> E. t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )
 
Theoremmapdpglem2a 35211* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   =>    |- ( ph -> t e. F )
 
Theoremmapdpglem3 35212* Lemma for mapdpg 35243. Baer p. 45, line 3: "infer...the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d g w z ph locally to avoid clashes with later substitutions into ph.) (Contributed by NM, 18-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   =>    |- ( ph -> E. g e. B E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) )
 
Theoremmapdpglem4N 35213* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( X .- Y ) =/= Q )
 
Theoremmapdpglem5N 35214* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   =>    |- ( ph -> t =/= ( 0g ` C ) )
 
Theoremmapdpglem6 35215* Lemma for mapdpg 35243. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> g = .0. )   =>    |- ( ph -> t e. ( M ` ( N ` { Y } ) ) )
 
Theoremmapdpglem8 35216* Lemma for mapdpg 35243. Baer p. 45, line 4: "...so that (F(x-y))* =< (Fy)*. This would imply that F(x-y) =< F(y)..." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> g = .0. )   =>    |- ( ph -> ( N ` { ( X .- Y ) } ) C_ ( N ` { Y } ) )
 
Theoremmapdpglem9 35217* Lemma for mapdpg 35243. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> g = .0. )   =>    |- ( ph -> X e. ( N ` { Y } ) )
 
Theoremmapdpglem10 35218* Lemma for mapdpg 35243. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> g = .0. )   =>    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
 
Theoremmapdpglem11 35219* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   =>    |- ( ph -> g =/= .0. )
 
Theoremmapdpglem12 35220* Lemma for mapdpg 35243. TODO: Can some commonality with mapdpglem6 35215 through mapdpglem11 35219 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- ( ph -> z = ( 0g ` C ) )   =>    |- ( ph -> t e. ( M ` ( N ` { X } ) ) )
 
Theoremmapdpglem13 35221* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- ( ph -> z = ( 0g ` C ) )   =>    |- ( ph -> ( N ` { ( X .- Y ) } ) C_ ( N ` { X } ) )
 
Theoremmapdpglem14 35222* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- ( ph -> z = ( 0g ` C ) )   =>    |- ( ph -> Y e. ( N ` { X } ) )
 
Theoremmapdpglem15 35223* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- ( ph -> z = ( 0g ` C ) )   =>    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
 
Theoremmapdpglem16 35224* Lemma for mapdpg 35243. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   =>    |- ( ph -> z =/= ( 0g ` C ) )
 
Theoremmapdpglem17N 35225* Lemma for mapdpg 35243. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> E e. F )
 
Theoremmapdpglem18 35226* Lemma for mapdpg 35243. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> E =/= ( 0g ` C ) )
 
Theoremmapdpglem19 35227* Lemma for mapdpg 35243. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> E e. ( M ` ( N ` { Y } ) ) )
 
Theoremmapdpglem20 35228* Lemma for mapdpg 35243. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { E } ) )
 
Theoremmapdpglem21 35229* Lemma for mapdpg 35243. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> ( ( ( invr ` A ) ` g ) .x. t ) = ( G R E ) )
 
Theoremmapdpglem22 35230* Lemma for mapdpg 35243. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R E ) } ) )
 
Theoremmapdpglem23 35231* Lemma for mapdpg 35243. Baer p. 45, line 10: "and so y' meets all our requirements." Our h is Baer's y'. (Contributed by NM, 20-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- .(+) = ( LSSum ` C )   &    |- J = ( LSpan ` C )   &    |- F = ( Base ` C )   &    |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- R = ( -g ` C )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- Q = ( 0g ` U )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )   &    |- .0. = ( 0g ` A )   &    |- ( ph -> g e. B )   &    |- ( ph -> z e. ( M ` ( N ` { Y } ) ) )   &    |- ( ph -> t = ( ( g .x. G ) R z ) )   &    |- ( ph -> X =/= Q )   &    |- ( ph -> Y =/= Q )   &    |- E = ( ( ( invr ` A ) ` g ) .x. z )   =>    |- ( ph -> E. h e. F ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) )
 
Theoremmapdpglem30a 35232 Lemma for mapdpg 35243. (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   =>    |- ( ph -> G =/= ( 0g ` C ) )
 
Theoremmapdpglem30b 35233 Lemma for mapdpg 35243. (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   =>    |- ( ph -> i =/= ( 0g ` C ) )
 
Theoremmapdpglem25 35234 Lemma for mapdpg 35243. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   =>    |- ( ph -> ( ( J ` { h } ) = ( J ` { i } ) /\ ( J ` { ( G R h ) } ) = ( J ` { ( G R i ) } ) ) )
 
Theoremmapdpglem26 35235* Lemma for mapdpg 35243. Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope $d u ph locally to avoid clashes with later substitutions into ph.) (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` A )   =>    |- ( ph -> E. u e. ( B \ { O } ) h = ( u .x. i ) )
 
Theoremmapdpglem27 35236* Lemma for mapdpg 35243. Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` A )   =>    |- ( ph -> E. v e. ( B \ { O } ) ( G R h ) = ( v .x. ( G R i ) ) )
 
Theoremmapdpglem29 35237* Lemma for mapdpg 35243. Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` A )   &    |- ( ph -> v e. B )   &    |- ( ph -> h = ( u .x. i ) )   &    |- ( ph -> ( G R h ) = ( v .x. ( G R i ) ) )   =>    |- ( ph -> ( J ` { G } ) =/= ( J ` { i } ) )
 
Theoremmapdpglem28 35238* Lemma for mapdpg 35243. Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` A )   &    |- ( ph -> v e. B )   &    |- ( ph -> h = ( u .x. i ) )   &    |- ( ph -> ( G R h ) = ( v .x. ( G R i ) ) )   =>    |- ( ph -> ( ( v .x. G ) R ( v .x. i ) ) = ( G R ( u .x. i ) ) )
 
Theoremmapdpglem30 35239* Lemma for mapdpg 35243. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 35238, using lvecindp2 18361) that v = 1 and v = u...". TODO: would it be shorter to have only the v = ( 1r ` A ) part and use mapdpglem28.u2 in mapdpglem31 35240? (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` A )   &    |- ( ph -> v e. B )   &    |- ( ph -> h = ( u .x. i ) )   &    |- ( ph -> ( G R h ) = ( v .x. ( G R i ) ) )   &    |- ( ph -> u e. B )   =>    |- ( ph -> ( v = ( 1r ` A ) /\ v = u ) )
 
Theoremmapdpglem31 35240* Lemma for mapdpg 35243. Baer p. 45 line 19: "...and we have consequently that y' = y'', as we claimed." (Contributed by NM, 23-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   &    |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) )   &    |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) )   &    |- A = (Scalar ` U )   &    |- B = ( Base ` A )   &    |- .x. = ( .s ` C )   &    |- O = ( 0g ` A )   &    |- ( ph -> v e. B )   &    |- ( ph -> h = ( u .x. i ) )   &    |- ( ph -> ( G R h ) = ( v .x. ( G R i ) ) )   &    |- ( ph -> u e. B )   =>    |- ( ph -> h = i )
 
Theoremmapdpglem24 35241* Lemma for mapdpg 35243. Existence part - consolidate hypotheses in mapdpglem23 35231. (Contributed by NM, 21-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   =>    |- ( ph -> E. h e. F ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) )
 
Theoremmapdpglem32 35242* Lemma for mapdpg 35243. Uniqueness part - consolidate hypotheses in mapdpglem31 35240. (Contributed by NM, 23-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   =>    |- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> h = i )
 
Theoremmapdpg 35243* Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in [Baer] p. 44. Our notation corresponds to Baer's as follows: M for *, N ` { } for F(), J ` { } for G(), X for x, G for x', Y for y, h for y'. TODO: Rename variables per mapdhval 35261. (Contributed by NM, 22-Mar-2015.)
|- H = ( LHyp ` K )   &    |- M = ( (mapd ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- F = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. F )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )   =>    |- ( ph -> E! h e. F ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) )
 
Theorembaerlem3lem1 35244 Lemma for baerlem3 35250. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   &    |- ( ph -> a e. B )   &    |- ( ph -> b e. B )   &    |- ( ph -> d e. B )   &    |- ( ph -> e e. B )   &    |- ( ph -> j = ( ( a .x. Y ) .+ ( b .x. Z ) ) )   &    |- ( ph -> j = ( ( d .x. ( X .- Y ) ) .+ ( e .x. ( X .- Z ) ) ) )   =>    |- ( ph -> j = ( a .x. ( Y .- Z ) ) )
 
Theorembaerlem5alem1 35245 Lemma for baerlem5a 35251. (Contributed by NM, 13-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   &    |- ( ph -> a e. B )   &    |- ( ph -> b e. B )   &    |- ( ph -> d e. B )   &    |- ( ph -> e e. B )   &    |- ( ph -> j = ( ( a .x. ( X .- Y ) ) .+ ( b .x. Z ) ) )   &    |- ( ph -> j = ( ( d .x. ( X .- Z ) ) .+ ( e .x. Y ) ) )   =>    |- ( ph -> j = ( a .x. ( X .- ( Y .+ Z ) ) ) )
 
Theorembaerlem5blem1 35246 Lemma for baerlem5b 35252. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   &    |- ( ph -> a e. B )   &    |- ( ph -> b e. B )   &    |- ( ph -> d e. B )   &    |- ( ph -> e e. B )   &    |- ( ph -> j = ( ( a .x. Y ) .+ ( b .x. Z ) ) )   &    |- ( ph -> j = ( ( d .x. ( X .- ( Y .+ Z ) ) ) .+ ( e .x. X ) ) )   =>    |- ( ph -> j = ( ( I ` d ) .x. ( Y .+ Z ) ) )
 
Theorembaerlem3lem2 35247 Lemma for baerlem3 35250. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   =>    |- ( ph -> ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { ( X .- Z ) } ) ) ) )
 
Theorembaerlem5alem2 35248 Lemma for baerlem5a 35251. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   =>    |- ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )
 
Theorembaerlem5blem2 35249 Lemma for baerlem5b 35252. (Contributed by NM, 13-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- R = (Scalar ` W )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- L = ( -g ` R )   &    |- Q = ( 0g ` R )   &    |- I = ( invg ` R )   =>    |- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )
 
Theorembaerlem3 35250 An equality that holds when X, Y, Z are independent (non-colinear) vectors. Part (3) in [Baer] p. 45. TODO fix ref. (Contributed by NM, 9-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   =>    |- ( ph -> ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { ( X .- Z ) } ) ) ) )
 
Theorembaerlem5a 35251 An equality that holds when X, Y, Z are independent (non-colinear) vectors. First equation of part (5) in [Baer] p. 46. (Contributed by NM, 10-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )
 
Theorembaerlem5b 35252 An equality that holds when X, Y, Z are independent (non-colinear) vectors. Second equation of part (5) in [Baer] p. 46. (Contributed by NM, 13-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .+ Z ) ) } ) .(+) ( N ` { X } ) ) ) )
 
Theorembaerlem5amN 35253 An equality that holds when X, Y, Z are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 35255 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- .+ = ( +g ` W )   =>    |- ( ph -> ( N ` { ( X .- ( Y .- Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .+ Z ) } ) .(+) ( N ` { Y } ) ) ) )
 
Theorembaerlem5bmN 35254 An equality that holds when X, Y, Z are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 35255 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   &    |- .(+) = ( LSSum ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( N `