hdmaprnlem9N

Description: Part of proof of part 12 in Baer p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 and mapdcnv11N . Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem1.h	\|- H = ( LHyp ` K )
	hdmaprnlem1.u	\|- U = ( ( DVecH ` K ) ` W )
	hdmaprnlem1.v	\|- V = ( Base ` U )
	hdmaprnlem1.n	\|- N = ( LSpan ` U )
	hdmaprnlem1.c	\|- C = ( ( LCDual ` K ) ` W )
	hdmaprnlem1.l	\|- L = ( LSpan ` C )
	hdmaprnlem1.m	\|- M = ( ( mapd ` K ) ` W )
	hdmaprnlem1.s	\|- S = ( ( HDMap ` K ) ` W )
	hdmaprnlem1.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmaprnlem1.se	\|- ( ph -> s e. ( D \ { Q } ) )
	hdmaprnlem1.ve	\|- ( ph -> v e. V )
	hdmaprnlem1.e	\|- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
	hdmaprnlem1.ue	\|- ( ph -> u e. V )
	hdmaprnlem1.un	\|- ( ph -> -. u e. ( N ` { v } ) )
	hdmaprnlem1.d	\|- D = ( Base ` C )
	hdmaprnlem1.q	\|- Q = ( 0g ` C )
	hdmaprnlem1.o	\|- .0. = ( 0g ` U )
	hdmaprnlem1.a	\|- .+b = ( +g ` C )
	hdmaprnlem1.t2	\|- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )
	hdmaprnlem1.p	\|- .+ = ( +g ` U )
	hdmaprnlem1.pt	\|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )
Assertion	hdmaprnlem9N	\|- ( ph -> s = ( S ` t ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem1.h	\|- H = ( LHyp ` K )
2		hdmaprnlem1.u	\|- U = ( ( DVecH ` K ) ` W )
3		hdmaprnlem1.v	\|- V = ( Base ` U )
4		hdmaprnlem1.n	\|- N = ( LSpan ` U )
5		hdmaprnlem1.c	\|- C = ( ( LCDual ` K ) ` W )
6		hdmaprnlem1.l	\|- L = ( LSpan ` C )
7		hdmaprnlem1.m	\|- M = ( ( mapd ` K ) ` W )
8		hdmaprnlem1.s	\|- S = ( ( HDMap ` K ) ` W )
9		hdmaprnlem1.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
10		hdmaprnlem1.se	\|- ( ph -> s e. ( D \ { Q } ) )
11		hdmaprnlem1.ve	\|- ( ph -> v e. V )
12		hdmaprnlem1.e	\|- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )
13		hdmaprnlem1.ue	\|- ( ph -> u e. V )
14		hdmaprnlem1.un	\|- ( ph -> -. u e. ( N ` { v } ) )
15		hdmaprnlem1.d	\|- D = ( Base ` C )
16		hdmaprnlem1.q	\|- Q = ( 0g ` C )
17		hdmaprnlem1.o	\|- .0. = ( 0g ` U )
18		hdmaprnlem1.a	\|- .+b = ( +g ` C )
19		hdmaprnlem1.t2	\|- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )
20		hdmaprnlem1.p	\|- .+ = ( +g ` U )
21		hdmaprnlem1.pt	\|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	hdmaprnlem7N	\|- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. ( L ` { ( ( S ` u ) .+b s ) } ) )
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	hdmaprnlem8N	\|- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. ( M ` ( N ` { t } ) ) )
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	hdmaprnlem4N	\|- ( ph -> ( M ` ( N ` { t } ) ) = ( L ` { s } ) )
25	23 24	eleqtrd	\|- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. ( L ` { s } ) )
26	22 25	elind	\|- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. ( ( L ` { ( ( S ` u ) .+b s ) } ) i^i ( L ` { s } ) ) )
27	1 5 9	lcdlvec	\|- ( ph -> C e. LVec )
28	1 5 9	lcdlmod	\|- ( ph -> C e. LMod )
29	1 2 3 5 15 8 9 13	hdmapcl	\|- ( ph -> ( S ` u ) e. D )
30	10	eldifad	\|- ( ph -> s e. D )
31	15 18	lmodvacl	\|- ( ( C e. LMod /\ ( S ` u ) e. D /\ s e. D ) -> ( ( S ` u ) .+b s ) e. D )
32	28 29 30 31	syl3anc	\|- ( ph -> ( ( S ` u ) .+b s ) e. D )
33		eqid	\|- ( LSubSp ` C ) = ( LSubSp ` C )
34	15 33 6	lspsncl	\|- ( ( C e. LMod /\ s e. D ) -> ( L ` { s } ) e. ( LSubSp ` C ) )
35	28 30 34	syl2anc	\|- ( ph -> ( L ` { s } ) e. ( LSubSp ` C ) )
36	1 7 5 33 9	mapdrn2	\|- ( ph -> ran M = ( LSubSp ` C ) )
37	35 36	eleqtrrd	\|- ( ph -> ( L ` { s } ) e. ran M )
38	1 7 9 37	mapdcnvid2	\|- ( ph -> ( M ` ( `' M ` ( L ` { s } ) ) ) = ( L ` { s } ) )
39	12 38	eqtr4d	\|- ( ph -> ( M ` ( N ` { v } ) ) = ( M ` ( `' M ` ( L ` { s } ) ) ) )
40		eqid	\|- ( LSubSp ` U ) = ( LSubSp ` U )
41	1 2 9	dvhlmod	\|- ( ph -> U e. LMod )
42	3 40 4	lspsncl	\|- ( ( U e. LMod /\ v e. V ) -> ( N ` { v } ) e. ( LSubSp ` U ) )
43	41 11 42	syl2anc	\|- ( ph -> ( N ` { v } ) e. ( LSubSp ` U ) )
44	1 7 2 40 9 37	mapdcnvcl	\|- ( ph -> ( `' M ` ( L ` { s } ) ) e. ( LSubSp ` U ) )
45	1 2 40 7 9 43 44	mapd11	\|- ( ph -> ( ( M ` ( N ` { v } ) ) = ( M ` ( `' M ` ( L ` { s } ) ) ) <-> ( N ` { v } ) = ( `' M ` ( L ` { s } ) ) ) )
46	39 45	mpbid	\|- ( ph -> ( N ` { v } ) = ( `' M ` ( L ` { s } ) ) )
47	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmaprnlem3N	\|- ( ph -> ( N ` { v } ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) )
48	46 47	eqnetrrd	\|- ( ph -> ( `' M ` ( L ` { s } ) ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) )
49	15 33 6	lspsncl	\|- ( ( C e. LMod /\ ( ( S ` u ) .+b s ) e. D ) -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSubSp ` C ) )
50	28 32 49	syl2anc	\|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSubSp ` C ) )
51	50 36	eleqtrrd	\|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ran M )
52	1 7 9 37 51	mapdcnv11N	\|- ( ph -> ( ( `' M ` ( L ` { s } ) ) = ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) <-> ( L ` { s } ) = ( L ` { ( ( S ` u ) .+b s ) } ) ) )
53	52	necon3bid	\|- ( ph -> ( ( `' M ` ( L ` { s } ) ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) <-> ( L ` { s } ) =/= ( L ` { ( ( S ` u ) .+b s ) } ) ) )
54	48 53	mpbid	\|- ( ph -> ( L ` { s } ) =/= ( L ` { ( ( S ` u ) .+b s ) } ) )
55	54	necomd	\|- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) =/= ( L ` { s } ) )
56	15 16 6 27 32 30 55	lspdisj2	\|- ( ph -> ( ( L ` { ( ( S ` u ) .+b s ) } ) i^i ( L ` { s } ) ) = { Q } )
57	26 56	eleqtrd	\|- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. { Q } )
58		elsni	\|- ( ( s ( -g ` C ) ( S ` t ) ) e. { Q } -> ( s ( -g ` C ) ( S ` t ) ) = Q )
59	57 58	syl	\|- ( ph -> ( s ( -g ` C ) ( S ` t ) ) = Q )
60	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	hdmaprnlem4tN	\|- ( ph -> t e. V )
61	1 2 3 5 15 8 9 60	hdmapcl	\|- ( ph -> ( S ` t ) e. D )
62		eqid	\|- ( -g ` C ) = ( -g ` C )
63	15 16 62	lmodsubeq0	\|- ( ( C e. LMod /\ s e. D /\ ( S ` t ) e. D ) -> ( ( s ( -g ` C ) ( S ` t ) ) = Q <-> s = ( S ` t ) ) )
64	28 30 61 63	syl3anc	\|- ( ph -> ( ( s ( -g ` C ) ( S ` t ) ) = Q <-> s = ( S ` t ) ) )
65	59 64	mpbid	\|- ( ph -> s = ( S ` t ) )

Metamath Proof Explorer

Theorem hdmaprnlem9N

Proof