mapdpglem20

Description: Lemma for mapdpg . Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	mapdpglem.h	\|- H = ( LHyp ` K )
	mapdpglem.m	\|- M = ( ( mapd ` K ) ` W )
	mapdpglem.u	\|- U = ( ( DVecH ` K ) ` W )
	mapdpglem.v	\|- V = ( Base ` U )
	mapdpglem.s	\|- .- = ( -g ` U )
	mapdpglem.n	\|- N = ( LSpan ` U )
	mapdpglem.c	\|- C = ( ( LCDual ` K ) ` W )
	mapdpglem.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	mapdpglem.x	\|- ( ph -> X e. V )
	mapdpglem.y	\|- ( ph -> Y e. V )
	mapdpglem1.p	\|- .(+) = ( LSSum ` C )
	mapdpglem2.j	\|- J = ( LSpan ` C )
	mapdpglem3.f	\|- F = ( Base ` C )
	mapdpglem3.te	\|- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
	mapdpglem3.a	\|- A = ( Scalar ` U )
	mapdpglem3.b	\|- B = ( Base ` A )
	mapdpglem3.t	\|- .x. = ( .s ` C )
	mapdpglem3.r	\|- R = ( -g ` C )
	mapdpglem3.g	\|- ( ph -> G e. F )
	mapdpglem3.e	\|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
	mapdpglem4.q	\|- Q = ( 0g ` U )
	mapdpglem.ne	\|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
	mapdpglem4.jt	\|- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )
	mapdpglem4.z	\|- .0. = ( 0g ` A )
	mapdpglem4.g4	\|- ( ph -> g e. B )
	mapdpglem4.z4	\|- ( ph -> z e. ( M ` ( N ` { Y } ) ) )
	mapdpglem4.t4	\|- ( ph -> t = ( ( g .x. G ) R z ) )
	mapdpglem4.xn	\|- ( ph -> X =/= Q )
	mapdpglem12.yn	\|- ( ph -> Y =/= Q )
	mapdpglem17.ep	\|- E = ( ( ( invr ` A ) ` g ) .x. z )
Assertion	mapdpglem20	\|- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { E } ) )

Proof

Step	Hyp	Ref	Expression
1		mapdpglem.h	\|- H = ( LHyp ` K )
2		mapdpglem.m	\|- M = ( ( mapd ` K ) ` W )
3		mapdpglem.u	\|- U = ( ( DVecH ` K ) ` W )
4		mapdpglem.v	\|- V = ( Base ` U )
5		mapdpglem.s	\|- .- = ( -g ` U )
6		mapdpglem.n	\|- N = ( LSpan ` U )
7		mapdpglem.c	\|- C = ( ( LCDual ` K ) ` W )
8		mapdpglem.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
9		mapdpglem.x	\|- ( ph -> X e. V )
10		mapdpglem.y	\|- ( ph -> Y e. V )
11		mapdpglem1.p	\|- .(+) = ( LSSum ` C )
12		mapdpglem2.j	\|- J = ( LSpan ` C )
13		mapdpglem3.f	\|- F = ( Base ` C )
14		mapdpglem3.te	\|- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
15		mapdpglem3.a	\|- A = ( Scalar ` U )
16		mapdpglem3.b	\|- B = ( Base ` A )
17		mapdpglem3.t	\|- .x. = ( .s ` C )
18		mapdpglem3.r	\|- R = ( -g ` C )
19		mapdpglem3.g	\|- ( ph -> G e. F )
20		mapdpglem3.e	\|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
21		mapdpglem4.q	\|- Q = ( 0g ` U )
22		mapdpglem.ne	\|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
23		mapdpglem4.jt	\|- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) )
24		mapdpglem4.z	\|- .0. = ( 0g ` A )
25		mapdpglem4.g4	\|- ( ph -> g e. B )
26		mapdpglem4.z4	\|- ( ph -> z e. ( M ` ( N ` { Y } ) ) )
27		mapdpglem4.t4	\|- ( ph -> t = ( ( g .x. G ) R z ) )
28		mapdpglem4.xn	\|- ( ph -> X =/= Q )
29		mapdpglem12.yn	\|- ( ph -> Y =/= Q )
30		mapdpglem17.ep	\|- E = ( ( ( invr ` A ) ` g ) .x. z )
31		eqid	\|- ( 0g ` C ) = ( 0g ` C )
32		eqid	\|- ( LSAtoms ` C ) = ( LSAtoms ` C )
33	1 7 8	lcdlvec	\|- ( ph -> C e. LVec )
34		eqid	\|- ( LSAtoms ` U ) = ( LSAtoms ` U )
35	1 3 8	dvhlmod	\|- ( ph -> U e. LMod )
36		eldifsn	\|- ( Y e. ( V \ { Q } ) <-> ( Y e. V /\ Y =/= Q ) )
37	10 29 36	sylanbrc	\|- ( ph -> Y e. ( V \ { Q } ) )
38	4 6 21 34 35 37	lsatlspsn	\|- ( ph -> ( N ` { Y } ) e. ( LSAtoms ` U ) )
39	1 2 3 34 7 32 8 38	mapdat	\|- ( ph -> ( M ` ( N ` { Y } ) ) e. ( LSAtoms ` C ) )
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30	mapdpglem19	\|- ( ph -> E e. ( M ` ( N ` { Y } ) ) )
41	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30	mapdpglem18	\|- ( ph -> E =/= ( 0g ` C ) )
42	31 12 32 33 39 40 41	lsatel	\|- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { E } ) )

Metamath Proof Explorer

Theorem mapdpglem20

Proof