Theorem lcfrlem16

Description: Lemma for lcfr . (Contributed by NM, 8-Mar-2015)

	Ref	Expression
Hypotheses	lcf1o.h	|- H = ( LHyp ` K )
	lcf1o.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcf1o.u	|- U = ( ( DVecH ` K ) ` W )
	lcf1o.v	|- V = ( Base ` U )
	lcf1o.a	|- .+ = ( +g ` U )
	lcf1o.t	|- .x. = ( .s ` U )
	lcf1o.s	|- S = ( Scalar ` U )
	lcf1o.r	|- R = ( Base ` S )
	lcf1o.z	|- .0. = ( 0g ` U )
	lcf1o.f	|- F = ( LFnl ` U )
	lcf1o.l	|- L = ( LKer ` U )
	lcf1o.d	|- D = ( LDual ` U )
	lcf1o.q	|- Q = ( 0g ` D )
	lcf1o.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
	lcf1o.j	|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
	lcflo.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfrlem16.p	|- P = ( LSubSp ` D )
	lcfrlem16.g	|- ( ph -> G e. P )
	lcfrlem16.gs	|- ( ph -> G C_ C )
	lcfrlem16.m	|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
	lcfrlem16.x	|- ( ph -> X e. ( E \ { .0. } ) )
Assertion	lcfrlem16	|- ( ph -> ( J ` X ) e. G )

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	|- H = ( LHyp ` K )
2		lcf1o.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcf1o.u	|- U = ( ( DVecH ` K ) ` W )
4		lcf1o.v	|- V = ( Base ` U )
5		lcf1o.a	|- .+ = ( +g ` U )
6		lcf1o.t	|- .x. = ( .s ` U )
7		lcf1o.s	|- S = ( Scalar ` U )
8		lcf1o.r	|- R = ( Base ` S )
9		lcf1o.z	|- .0. = ( 0g ` U )
10		lcf1o.f	|- F = ( LFnl ` U )
11		lcf1o.l	|- L = ( LKer ` U )
12		lcf1o.d	|- D = ( LDual ` U )
13		lcf1o.q	|- Q = ( 0g ` D )
14		lcf1o.c	|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
15		lcf1o.j	|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
16		lcflo.k	|- ( ph -> ( K e. HL /\ W e. H ) )
17		lcfrlem16.p	|- P = ( LSubSp ` D )
18		lcfrlem16.g	|- ( ph -> G e. P )
19		lcfrlem16.gs	|- ( ph -> G C_ C )
20		lcfrlem16.m	|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
21		lcfrlem16.x	|- ( ph -> X e. ( E \ { .0. } ) )
22	21	eldifad	|- ( ph -> X e. E )
23	22 20	eleqtrdi	|- ( ph -> X e. U_ g e. G ( ._|_ ` ( L ` g ) ) )
24		eliun	|- ( X e. U_ g e. G ( ._|_ ` ( L ` g ) ) <-> E. g e. G X e. ( ._|_ ` ( L ` g ) ) )
25	23 24	sylib	|- ( ph -> E. g e. G X e. ( ._|_ ` ( L ` g ) ) )
26		eqid	|- ( .s ` D ) = ( .s ` D )
27	1 3 16	dvhlvec	|- ( ph -> U e. LVec )
28	27	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> U e. LVec )
29		eqid	|- ( Base ` D ) = ( Base ` D )
30	29 17	lssel	|- ( ( G e. P /\ g e. G ) -> g e. ( Base ` D ) )
31	18 30	sylan	|- ( ( ph /\ g e. G ) -> g e. ( Base ` D ) )
32	1 3 16	dvhlmod	|- ( ph -> U e. LMod )
33	10 12 29 32	ldualvbase	|- ( ph -> ( Base ` D ) = F )
34	33	adantr	|- ( ( ph /\ g e. G ) -> ( Base ` D ) = F )
35	31 34	eleqtrd	|- ( ( ph /\ g e. G ) -> g e. F )
36	35	3adant3	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> g e. F )
37	16	adantr	|- ( ( ph /\ g e. G ) -> ( K e. HL /\ W e. H ) )
38	32	adantr	|- ( ( ph /\ g e. G ) -> U e. LMod )
39	4 10 11 38 35	lkrssv	|- ( ( ph /\ g e. G ) -> ( L ` g ) C_ V )
40	1 3 4 2	dochssv	|- ( ( ( K e. HL /\ W e. H ) /\ ( L ` g ) C_ V ) -> ( ._|_ ` ( L ` g ) ) C_ V )
41	37 39 40	syl2anc	|- ( ( ph /\ g e. G ) -> ( ._|_ ` ( L ` g ) ) C_ V )
42	41	ralrimiva	|- ( ph -> A. g e. G ( ._|_ ` ( L ` g ) ) C_ V )
43		iunss	|- ( U_ g e. G ( ._|_ ` ( L ` g ) ) C_ V <-> A. g e. G ( ._|_ ` ( L ` g ) ) C_ V )
44	42 43	sylibr	|- ( ph -> U_ g e. G ( ._|_ ` ( L ` g ) ) C_ V )
45	20 44	eqsstrid	|- ( ph -> E C_ V )
46	45	ssdifd	|- ( ph -> ( E \ { .0. } ) C_ ( V \ { .0. } ) )
47	46 21	sseldd	|- ( ph -> X e. ( V \ { .0. } ) )
48	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem10	|- ( ph -> ( J ` X ) e. F )
49	48	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( J ` X ) e. F )
50		eqid	|- ( LSAtoms ` U ) = ( LSAtoms ` U )
51	16	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( K e. HL /\ W e. H ) )
52		simp3	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> X e. ( ._|_ ` ( L ` g ) ) )
53		eldifsni	|- ( X e. ( E \ { .0. } ) -> X =/= .0. )
54	21 53	syl	|- ( ph -> X =/= .0. )
55	54	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> X =/= .0. )
56		eldifsn	|- ( X e. ( ( ._|_ ` ( L ` g ) ) \ { .0. } ) <-> ( X e. ( ._|_ ` ( L ` g ) ) /\ X =/= .0. ) )
57	52 55 56	sylanbrc	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> X e. ( ( ._|_ ` ( L ` g ) ) \ { .0. } ) )
58	1 2 3 4 9 10 11 51 36 57 50	dochsnkrlem2	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( ._|_ ` ( L ` g ) ) e. ( LSAtoms ` U ) )
59	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem15	|- ( ph -> X e. ( ._|_ ` ( L ` ( J ` X ) ) ) )
60		eldifsn	|- ( X e. ( ( ._|_ ` ( L ` ( J ` X ) ) ) \ { .0. } ) <-> ( X e. ( ._|_ ` ( L ` ( J ` X ) ) ) /\ X =/= .0. ) )
61	59 54 60	sylanbrc	|- ( ph -> X e. ( ( ._|_ ` ( L ` ( J ` X ) ) ) \ { .0. } ) )
62	1 2 3 4 9 10 11 16 48 61 50	dochsnkrlem2	|- ( ph -> ( ._|_ ` ( L ` ( J ` X ) ) ) e. ( LSAtoms ` U ) )
63	62	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( ._|_ ` ( L ` ( J ` X ) ) ) e. ( LSAtoms ` U ) )
64	59	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> X e. ( ._|_ ` ( L ` ( J ` X ) ) ) )
65	9 50 28 58 63 55 52 64	lsat2el	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( ._|_ ` ( L ` g ) ) = ( ._|_ ` ( L ` ( J ` X ) ) ) )
66		eqid	|- ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
67	19	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> G C_ C )
68		simp2	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> g e. G )
69	67 68	sseldd	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> g e. C )
70	1 66 2 3 10 11 14 51 36	lcfl5	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( g e. C <-> ( L ` g ) e. ran ( ( DIsoH ` K ) ` W ) ) )
71	69 70	mpbid	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( L ` g ) e. ran ( ( DIsoH ` K ) ` W ) )
72	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem13	|- ( ph -> ( J ` X ) e. ( C \ { Q } ) )
73	72	eldifad	|- ( ph -> ( J ` X ) e. C )
74	1 66 2 3 10 11 14 16 48	lcfl5	|- ( ph -> ( ( J ` X ) e. C <-> ( L ` ( J ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) ) )
75	73 74	mpbid	|- ( ph -> ( L ` ( J ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
76	75	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( L ` ( J ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
77	1 66 2 51 71 76	doch11	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( ( ._|_ ` ( L ` g ) ) = ( ._|_ ` ( L ` ( J ` X ) ) ) <-> ( L ` g ) = ( L ` ( J ` X ) ) ) )
78	65 77	mpbid	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( L ` g ) = ( L ` ( J ` X ) ) )
79	7 8 10 11 12 26 28 36 49 78	eqlkr4	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> E. k e. R ( J ` X ) = ( k ( .s ` D ) g ) )
80	32	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> U e. LMod )
81	80	adantr	|- ( ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) /\ k e. R ) -> U e. LMod )
82	18	3ad2ant1	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> G e. P )
83	82	adantr	|- ( ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) /\ k e. R ) -> G e. P )
84		simpr	|- ( ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) /\ k e. R ) -> k e. R )
85		simpl2	|- ( ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) /\ k e. R ) -> g e. G )
86	7 8 12 26 17 81 83 84 85	ldualssvscl	|- ( ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) /\ k e. R ) -> ( k ( .s ` D ) g ) e. G )
87		eleq1	|- ( ( J ` X ) = ( k ( .s ` D ) g ) -> ( ( J ` X ) e. G <-> ( k ( .s ` D ) g ) e. G ) )
88	86 87	syl5ibrcom	|- ( ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) /\ k e. R ) -> ( ( J ` X ) = ( k ( .s ` D ) g ) -> ( J ` X ) e. G ) )
89	88	rexlimdva	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( E. k e. R ( J ` X ) = ( k ( .s ` D ) g ) -> ( J ` X ) e. G ) )
90	79 89	mpd	|- ( ( ph /\ g e. G /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( J ` X ) e. G )
91	90	rexlimdv3a	|- ( ph -> ( E. g e. G X e. ( ._|_ ` ( L ` g ) ) -> ( J ` X ) e. G ) )
92	25 91	mpd	|- ( ph -> ( J ` X ) e. G )