Theorem lcfrlem4

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

	Ref	Expression
Hypotheses	lcfrlem4.h	|- H = ( LHyp ` K )
	lcfrlem4.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcfrlem4.u	|- U = ( ( DVecH ` K ) ` W )
	lcfrlem4.v	|- V = ( Base ` U )
	lcfrlem4.l	|- L = ( LKer ` U )
	lcfrlem4.d	|- D = ( LDual ` U )
	lcfrlem4.q	|- Q = ( LSubSp ` D )
	lcfrlem4.e	|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
	lcfrlem4.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfrlem4.g	|- ( ph -> G e. Q )
	lcfrlem4.x	|- ( ph -> X e. E )
Assertion	lcfrlem4	|- ( ph -> X e. V )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem4.h	|- H = ( LHyp ` K )
2		lcfrlem4.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcfrlem4.u	|- U = ( ( DVecH ` K ) ` W )
4		lcfrlem4.v	|- V = ( Base ` U )
5		lcfrlem4.l	|- L = ( LKer ` U )
6		lcfrlem4.d	|- D = ( LDual ` U )
7		lcfrlem4.q	|- Q = ( LSubSp ` D )
8		lcfrlem4.e	|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
9		lcfrlem4.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcfrlem4.g	|- ( ph -> G e. Q )
11		lcfrlem4.x	|- ( ph -> X e. E )
12	9	adantr	|- ( ( ph /\ g e. G ) -> ( K e. HL /\ W e. H ) )
13		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
14	1 3 9	dvhlmod	|- ( ph -> U e. LMod )
15	14	adantr	|- ( ( ph /\ g e. G ) -> U e. LMod )
16		eqid	|- ( Base ` D ) = ( Base ` D )
17	16 7	lssel	|- ( ( G e. Q /\ g e. G ) -> g e. ( Base ` D ) )
18	10 17	sylan	|- ( ( ph /\ g e. G ) -> g e. ( Base ` D ) )
19	13 6 16 14	ldualvbase	|- ( ph -> ( Base ` D ) = ( LFnl ` U ) )
20	19	adantr	|- ( ( ph /\ g e. G ) -> ( Base ` D ) = ( LFnl ` U ) )
21	18 20	eleqtrd	|- ( ( ph /\ g e. G ) -> g e. ( LFnl ` U ) )
22	4 13 5 15 21	lkrssv	|- ( ( ph /\ g e. G ) -> ( L ` g ) C_ V )
23	1 3 4 2	dochssv	|- ( ( ( K e. HL /\ W e. H ) /\ ( L ` g ) C_ V ) -> ( ._|_ ` ( L ` g ) ) C_ V )
24	12 22 23	syl2anc	|- ( ( ph /\ g e. G ) -> ( ._|_ ` ( L ` g ) ) C_ V )
25	24	ralrimiva	|- ( ph -> A. g e. G ( ._|_ ` ( L ` g ) ) C_ V )
26		iunss	|- ( U_ g e. G ( ._|_ ` ( L ` g ) ) C_ V <-> A. g e. G ( ._|_ ` ( L ` g ) ) C_ V )
27	25 26	sylibr	|- ( ph -> U_ g e. G ( ._|_ ` ( L ` g ) ) C_ V )
28	11 8	eleqtrdi	|- ( ph -> X e. U_ g e. G ( ._|_ ` ( L ` g ) ) )
29	27 28	sseldd	|- ( ph -> X e. V )