lcfrlem41

Description: Lemma for lcfr . Eliminate span condition. (Contributed by NM, 11-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem38.h	\|- H = ( LHyp ` K )
	lcfrlem38.o	\|- ._\|_ = ( ( ocH ` K ) ` W )
	lcfrlem38.u	\|- U = ( ( DVecH ` K ) ` W )
	lcfrlem38.p	\|- .+ = ( +g ` U )
	lcfrlem38.f	\|- F = ( LFnl ` U )
	lcfrlem38.l	\|- L = ( LKer ` U )
	lcfrlem38.d	\|- D = ( LDual ` U )
	lcfrlem38.q	\|- Q = ( LSubSp ` D )
	lcfrlem38.c	\|- C = { f e. ( LFnl ` U ) \| ( ._\|_ ` ( ._\|_ ` ( L ` f ) ) ) = ( L ` f ) }
	lcfrlem38.e	\|- E = U_ g e. G ( ._\|_ ` ( L ` g ) )
	lcfrlem38.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfrlem38.g	\|- ( ph -> G e. Q )
	lcfrlem38.gs	\|- ( ph -> G C_ C )
	lcfrlem38.xe	\|- ( ph -> X e. E )
	lcfrlem38.ye	\|- ( ph -> Y e. E )
	lcfrlem38.z	\|- .0. = ( 0g ` U )
	lcfrlem38.x	\|- ( ph -> X =/= .0. )
	lcfrlem38.y	\|- ( ph -> Y =/= .0. )
Assertion	lcfrlem41	\|- ( ph -> ( X .+ Y ) e. E )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem38.h	\|- H = ( LHyp ` K )
2		lcfrlem38.o	\|- ._\|_ = ( ( ocH ` K ) ` W )
3		lcfrlem38.u	\|- U = ( ( DVecH ` K ) ` W )
4		lcfrlem38.p	\|- .+ = ( +g ` U )
5		lcfrlem38.f	\|- F = ( LFnl ` U )
6		lcfrlem38.l	\|- L = ( LKer ` U )
7		lcfrlem38.d	\|- D = ( LDual ` U )
8		lcfrlem38.q	\|- Q = ( LSubSp ` D )
9		lcfrlem38.c	\|- C = { f e. ( LFnl ` U ) \| ( ._\|_ ` ( ._\|_ ` ( L ` f ) ) ) = ( L ` f ) }
10		lcfrlem38.e	\|- E = U_ g e. G ( ._\|_ ` ( L ` g ) )
11		lcfrlem38.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
12		lcfrlem38.g	\|- ( ph -> G e. Q )
13		lcfrlem38.gs	\|- ( ph -> G C_ C )
14		lcfrlem38.xe	\|- ( ph -> X e. E )
15		lcfrlem38.ye	\|- ( ph -> Y e. E )
16		lcfrlem38.z	\|- .0. = ( 0g ` U )
17		lcfrlem38.x	\|- ( ph -> X =/= .0. )
18		lcfrlem38.y	\|- ( ph -> Y =/= .0. )
19		eqid	\|- ( LSpan ` U ) = ( LSpan ` U )
20	11	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) ) -> ( K e. HL /\ W e. H ) )
21	12	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) ) -> G e. Q )
22	14	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) ) -> X e. E )
23	15	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) ) -> Y e. E )
24		simpr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) ) -> ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) )
25	1 2 3 4 19 6 7 8 20 21 10 22 23 24	lcfrlem6	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) = ( ( LSpan ` U ) ` { Y } ) ) -> ( X .+ Y ) e. E )
26	11	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> ( K e. HL /\ W e. H ) )
27	12	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> G e. Q )
28	13	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> G C_ C )
29	14	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> X e. E )
30	15	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> Y e. E )
31	17	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> X =/= .0. )
32	18	adantr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> Y =/= .0. )
33		simpr	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) )
34	1 2 3 4 5 6 7 8 9 10 26 27 28 29 30 16 31 32 19 33	lcfrlem40	\|- ( ( ph /\ ( ( LSpan ` U ) ` { X } ) =/= ( ( LSpan ` U ) ` { Y } ) ) -> ( X .+ Y ) e. E )
35	25 34	pm2.61dane	\|- ( ph -> ( X .+ Y ) e. E )

Metamath Proof Explorer

Theorem lcfrlem41

Proof