lcfrlem42

Description: Lemma for lcfr . Eliminate nonzero 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 )
Assertion	lcfrlem42	\|- ( 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	1 3 11	dvhlmod	\|- ( ph -> U e. LMod )
17		eqid	\|- ( Base ` U ) = ( Base ` U )
18	1 2 3 17 6 7 8 10 11 12 14	lcfrlem4	\|- ( ph -> X e. ( Base ` U ) )
19	1 2 3 17 6 7 8 10 11 12 15	lcfrlem4	\|- ( ph -> Y e. ( Base ` U ) )
20	17 4	lmodcom	\|- ( ( U e. LMod /\ X e. ( Base ` U ) /\ Y e. ( Base ` U ) ) -> ( X .+ Y ) = ( Y .+ X ) )
21	16 18 19 20	syl3anc	\|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )
22	21	adantr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( X .+ Y ) = ( Y .+ X ) )
23	11	adantr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
24	12	adantr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> G e. Q )
25	15	adantr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> Y e. E )
26		eqid	\|- ( 0g ` U ) = ( 0g ` U )
27		simpr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> X = ( 0g ` U ) )
28	1 2 3 4 6 7 8 23 24 10 25 26 27	lcfrlem7	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( Y .+ X ) e. E )
29	22 28	eqeltrd	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( X .+ Y ) e. E )
30	11	adantr	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
31	12	adantr	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> G e. Q )
32	14	adantr	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> X e. E )
33		simpr	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> Y = ( 0g ` U ) )
34	1 2 3 4 6 7 8 30 31 10 32 26 33	lcfrlem7	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> ( X .+ Y ) e. E )
35	11	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )
36	12	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> G e. Q )
37	13	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> G C_ C )
38	14	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X e. E )
39	15	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y e. E )
40		simprl	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )
41		simprr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )
42	1 2 3 4 5 6 7 8 9 10 35 36 37 38 39 26 40 41	lcfrlem41	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( X .+ Y ) e. E )
43	29 34 42	pm2.61da2ne	\|- ( ph -> ( X .+ Y ) e. E )

Metamath Proof Explorer

Theorem lcfrlem42

Proof