Metamath Proof Explorer

Theorem lcfrlem40

Description: Lemma for lcfr . Eliminate B and I . (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. )
lcfrlem38.sp 
|- N = ( LSpan ` U )
lcfrlem38.ne 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion lcfrlem40 
|- ( 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 lcfrlem38.sp 
 |-  N = ( LSpan ` U )
20 lcfrlem38.ne 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
21 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
22 1 3 11 dvhlmod 
 |-  ( ph -> U e. LMod )
23 eqid 
 |-  ( Base ` U ) = ( Base ` U )
24 1 2 3 23 6 7 8 10 11 12 14 lcfrlem4 
 |-  ( ph -> X e. ( Base ` U ) )
25 eldifsn 
 |-  ( X e. ( ( Base ` U ) \ { .0. } ) <-> ( X e. ( Base ` U ) /\ X =/= .0. ) )
26 24 17 25 sylanbrc 
 |-  ( ph -> X e. ( ( Base ` U ) \ { .0. } ) )
27 1 2 3 23 6 7 8 10 11 12 15 lcfrlem4 
 |-  ( ph -> Y e. ( Base ` U ) )
28 eldifsn 
 |-  ( Y e. ( ( Base ` U ) \ { .0. } ) <-> ( Y e. ( Base ` U ) /\ Y =/= .0. ) )
29 27 18 28 sylanbrc 
 |-  ( ph -> Y e. ( ( Base ` U ) \ { .0. } ) )
30 1 2 3 23 4 16 19 21 11 26 29 20 lcfrlem21 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. ( LSAtoms ` U ) )
31 16 21 22 30 lsateln0 
 |-  ( ph -> E. i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) i =/= .0. )
32 11 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> ( K e. HL /\ W e. H ) )
33 12 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> G e. Q )
34 13 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> G C_ C )
35 14 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> X e. E )
36 15 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> Y e. E )
37 17 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> X =/= .0. )
38 18 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> Y =/= .0. )
39 20 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
40 eqid 
 |-  ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
41 simp2 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) )
42 simp3 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> i =/= .0. )
43 1 2 3 4 5 6 7 8 9 10 32 33 34 35 36 16 37 38 19 39 40 41 42 lcfrlem39 
 |-  ( ( ph /\ i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) /\ i =/= .0. ) -> ( X .+ Y ) e. E )
44 43 rexlimdv3a 
 |-  ( ph -> ( E. i e. ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) i =/= .0. -> ( X .+ Y ) e. E ) )
45 31 44 mpd 
 |-  ( ph -> ( X .+ Y ) e. E )