P. 354 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35301-35400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mapdpglem17N 35301*	Lemma for mapdpg 35319. 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 )
Theorem	mapdpglem18 35302*	Lemma for mapdpg 35319. 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 ) )
Theorem	mapdpglem19 35303*	Lemma for mapdpg 35319. 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 } ) ) )
Theorem	mapdpglem20 35304*	Lemma for mapdpg 35319. 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 } ) )
Theorem	mapdpglem21 35305*	Lemma for mapdpg 35319. (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 ) )
Theorem	mapdpglem22 35306*	Lemma for mapdpg 35319. 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 ) } ) )
Theorem	mapdpglem23 35307*	Lemma for mapdpg 35319. 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 ) } ) ) )
Theorem	mapdpglem30a 35308	Lemma for mapdpg 35319. (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 ) )
Theorem	mapdpglem30b 35309	Lemma for mapdpg 35319. (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 ) )
Theorem	mapdpglem25 35310	Lemma for mapdpg 35319. 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 ) } ) ) )
Theorem	mapdpglem26 35311*	Lemma for mapdpg 35319. 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 ) )
Theorem	mapdpglem27 35312*	Lemma for mapdpg 35319. 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 ) ) )
Theorem	mapdpglem29 35313*	Lemma for mapdpg 35319. 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 } ) )
Theorem	mapdpglem28 35314*	Lemma for mapdpg 35319. 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 ) ) )
Theorem	mapdpglem30 35315*	Lemma for mapdpg 35319. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 35314, using lvecindp2 18411) 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 35316? (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 ) )
Theorem	mapdpglem31 35316*	Lemma for mapdpg 35319. 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 )
Theorem	mapdpglem24 35317*	Lemma for mapdpg 35319. Existence part - consolidate hypotheses in mapdpglem23 35307. (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 ) } ) ) )
Theorem	mapdpglem32 35318*	Lemma for mapdpg 35319. Uniqueness part - consolidate hypotheses in mapdpglem31 35316. (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 )
Theorem	mapdpg 35319*	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 35337. (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 ) } ) ) )
Theorem	baerlem3lem1 35320	Lemma for baerlem3 35326. (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 ) ) )
Theorem	baerlem5alem1 35321	Lemma for baerlem5a 35327. (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 ) ) ) )
Theorem	baerlem5blem1 35322	Lemma for baerlem5b 35328. (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 ) ) )
Theorem	baerlem3lem2 35323	Lemma for baerlem3 35326. (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 ) } ) ) ) )
Theorem	baerlem5alem2 35324	Lemma for baerlem5a 35327. (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 } ) ) ) )
Theorem	baerlem5blem2 35325	Lemma for baerlem5b 35328. (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 } ) ) ) )
Theorem	baerlem3 35326	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 ) } ) ) ) )
Theorem	baerlem5a 35327	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 } ) ) ) )
Theorem	baerlem5b 35328	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 } ) ) ) )
Theorem	baerlem5amN 35329	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 35331 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 } ) ) ) )
Theorem	baerlem5bmN 35330	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 35331 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 ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) )
Theorem	baerlem5abmN 35331	An equality that holds when X, Y, Z are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not be needed. (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 } ) ) ) /\ ( N ` { ( Y .- Z ) } ) = ( ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- ( Y .- Z ) ) } ) .(+) ( N ` { X } ) ) ) ) )
Theorem	mapdindp0 35332	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   &    |- ( ph -> ( Y .+ Z ) =/= .0. )   =>    |- ( ph -> ( N ` { ( Y .+ Z ) } ) = ( N ` { Y } ) )
Theorem	mapdindp1 35333	Vector independence lemma. (Contributed by NM, 1-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )
Theorem	mapdindp2 35334	Vector independence lemma. (Contributed by NM, 1-May-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> -. w e. ( N ` { X , ( Y .+ Z ) } ) )
Theorem	mapdindp3 35335	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> ( N ` { X } ) =/= ( N ` { ( w .+ Y ) } ) )
Theorem	mapdindp4 35336	Vector independence lemma. (Contributed by NM, 29-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> w e. ( V \ { .0. } ) )   &    |- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> -. w e. ( N ` { X , Y } ) )   =>    |- ( ph -> -. Z e. ( N ` { X , ( w .+ Y ) } ) )
Theorem	mapdhval 35337*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> X e. A )   &    |- ( ph -> F e. B )   &    |- ( ph -> Y e. E )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )
Theorem	mapdhval0 35338*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X e. A )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( I ` <. X , F , .0. >. ) = Q )
Theorem	mapdhval2 35339*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- ( ph -> X e. A )   &    |- ( ph -> F e. B )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
Theorem	mapdhcl 35340*	Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( I ` <. X , F , Y >. ) e. D )
Theorem	mapdheq 35341*	Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( ( M ` ( N ` { Y } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R G ) } ) ) ) )
Theorem	mapdheq2 35342*	Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G -> ( I ` <. Y , G , X >. ) = F ) )
Theorem	mapdheq2biN 35343*	Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 35342 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> G e. D )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )   =>    |- ( ph -> ( ( I ` <. X , F , Y >. ) = G <-> ( I ` <. Y , G , X >. ) = F ) )
Theorem	mapdheq4lem 35344*	Lemma for mapdheq4 35345. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( Y .- Z ) } ) ) = ( J ` { ( G R E ) } ) )
Theorem	mapdheq4 35345*	Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( I ` <. Y , G , Z >. ) = E )
Theorem	mapdh6lem1N 35346*	Lemma for mapdh6N 35360. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( X .- ( Y .+ Z ) ) } ) ) = ( J ` { ( F R ( G .+b E ) ) } ) )
Theorem	mapdh6lem2N 35347*	Lemma for mapdh6N 35360. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( M ` ( N ` { ( Y .+ Z ) } ) ) = ( J ` { ( G .+b E ) } ) )
Theorem	mapdh6aN 35348*	Lemma for mapdh6N 35360. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> Z e. ( V \ { .0. } ) )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   &    |- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   &    |- ( ph -> ( I ` <. X , F , Z >. ) = E )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6b0N 35349*	Lemmma for mapdh6N 35360. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> ( ( N ` { X } ) i^i ( N ` { Y , Z } ) ) = { .0. } )   =>    |- ( ph -> -. X e. ( N ` { Y , Z } ) )
Theorem	mapdh6bN 35350*	Lemmma for mapdh6N 35360. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` 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 \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> Y = .0. )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. X e. ( N ` { Y , Z } ) )   =>    |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )
Theorem	mapdh6cN 35351*	Lemmma for mapdh6N 35360. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
|- Q = ( 0g ` C )   &    |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   &    |- 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 )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- J = ( LSpan ` C )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J