Metamath Proof Explorer

Theorem lcfrlem6

Description: Lemma for lcfr . Closure of vector sum with colinear vectors. TODO: Move down N definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015)

Ref Expression
Hypotheses lcfrlem6.h 
|- H = ( LHyp ` K )
lcfrlem6.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfrlem6.u 
|- U = ( ( DVecH ` K ) ` W )
lcfrlem6.p 
|- .+ = ( +g ` U )
lcfrlem6.n 
|- N = ( LSpan ` U )
lcfrlem6.l 
|- L = ( LKer ` U )
lcfrlem6.d 
|- D = ( LDual ` U )
lcfrlem6.q 
|- Q = ( LSubSp ` D )
lcfrlem6.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrlem6.g 
|- ( ph -> G e. Q )
lcfrlem6.e 
|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
lcfrlem6.x 
|- ( ph -> X e. E )
lcfrlem6.y 
|- ( ph -> Y e. E )
lcfrlem6.en 
|- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
Assertion lcfrlem6 
|- ( ph -> ( X .+ Y ) e. E )

Proof

Step Hyp Ref Expression
1 lcfrlem6.h 
 |-  H = ( LHyp ` K )
2 lcfrlem6.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfrlem6.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfrlem6.p 
 |-  .+ = ( +g ` U )
5 lcfrlem6.n 
 |-  N = ( LSpan ` U )
6 lcfrlem6.l 
 |-  L = ( LKer ` U )
7 lcfrlem6.d 
 |-  D = ( LDual ` U )
8 lcfrlem6.q 
 |-  Q = ( LSubSp ` D )
9 lcfrlem6.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcfrlem6.g 
 |-  ( ph -> G e. Q )
11 lcfrlem6.e 
 |-  E = U_ g e. G ( ._|_ ` ( L ` g ) )
12 lcfrlem6.x 
 |-  ( ph -> X e. E )
13 lcfrlem6.y 
 |-  ( ph -> Y e. E )
14 lcfrlem6.en 
 |-  ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
15 12 11 eleqtrdi 
 |-  ( ph -> X e. U_ g e. G ( ._|_ ` ( L ` g ) ) )
16 eliun 
 |-  ( X e. U_ g e. G ( ._|_ ` ( L ` g ) ) <-> E. g e. G X e. ( ._|_ ` ( L ` g ) ) )
17 15 16 sylib 
 |-  ( ph -> E. g e. G X e. ( ._|_ ` ( L ` g ) ) )
18 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
19 18 adantr 
 |-  ( ( ph /\ g e. G ) -> U e. LMod )
20 19 adantr 
 |-  ( ( ( ph /\ g e. G ) /\ X e. ( ._|_ ` ( L ` g ) ) ) -> U e. LMod )
21 9 adantr 
 |-  ( ( ph /\ g e. G ) -> ( K e. HL /\ W e. H ) )
22 eqid 
 |-  ( Base ` U ) = ( Base ` U )
23 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
24 eqid 
 |-  ( Base ` D ) = ( Base ` D )
25 24 8 lssel 
 |-  ( ( G e. Q /\ g e. G ) -> g e. ( Base ` D ) )
26 10 25 sylan 
 |-  ( ( ph /\ g e. G ) -> g e. ( Base ` D ) )
27 23 7 24 18 ldualvbase 
 |-  ( ph -> ( Base ` D ) = ( LFnl ` U ) )
28 27 adantr 
 |-  ( ( ph /\ g e. G ) -> ( Base ` D ) = ( LFnl ` U ) )
29 26 28 eleqtrd 
 |-  ( ( ph /\ g e. G ) -> g e. ( LFnl ` U ) )
30 22 23 6 19 29 lkrssv 
 |-  ( ( ph /\ g e. G ) -> ( L ` g ) C_ ( Base ` U ) )
31 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
32 1 3 22 31 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` g ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` g ) ) e. ( LSubSp ` U ) )
33 21 30 32 syl2anc 
 |-  ( ( ph /\ g e. G ) -> ( ._|_ ` ( L ` g ) ) e. ( LSubSp ` U ) )
34 33 adantr 
 |-  ( ( ( ph /\ g e. G ) /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( ._|_ ` ( L ` g ) ) e. ( LSubSp ` U ) )
35 simpr 
 |-  ( ( ( ph /\ g e. G ) /\ X e. ( ._|_ ` ( L ` g ) ) ) -> X e. ( ._|_ ` ( L ` g ) ) )
36 14 adantr 
 |-  ( ( ph /\ g e. G ) -> ( N ` { X } ) = ( N ` { Y } ) )
37 36 adantr 
 |-  ( ( ( ph /\ g e. G ) /\ ( N ` { X } ) C_ ( ._|_ ` ( L ` g ) ) ) -> ( N ` { X } ) = ( N ` { Y } ) )
38 simpr 
 |-  ( ( ( ph /\ g e. G ) /\ ( N ` { X } ) C_ ( ._|_ ` ( L ` g ) ) ) -> ( N ` { X } ) C_ ( ._|_ ` ( L ` g ) ) )
39 37 38 eqsstrrd 
 |-  ( ( ( ph /\ g e. G ) /\ ( N ` { X } ) C_ ( ._|_ ` ( L ` g ) ) ) -> ( N ` { Y } ) C_ ( ._|_ ` ( L ` g ) ) )
40 39 ex 
 |-  ( ( ph /\ g e. G ) -> ( ( N ` { X } ) C_ ( ._|_ ` ( L ` g ) ) -> ( N ` { Y } ) C_ ( ._|_ ` ( L ` g ) ) ) )
41 1 2 3 22 6 7 8 11 9 10 12 lcfrlem4 
 |-  ( ph -> X e. ( Base ` U ) )
42 41 adantr 
 |-  ( ( ph /\ g e. G ) -> X e. ( Base ` U ) )
43 22 31 5 19 33 42 ellspsn5b 
 |-  ( ( ph /\ g e. G ) -> ( X e. ( ._|_ ` ( L ` g ) ) <-> ( N ` { X } ) C_ ( ._|_ ` ( L ` g ) ) ) )
44 1 2 3 22 6 7 8 11 9 10 13 lcfrlem4 
 |-  ( ph -> Y e. ( Base ` U ) )
45 44 adantr 
 |-  ( ( ph /\ g e. G ) -> Y e. ( Base ` U ) )
46 22 31 5 19 33 45 ellspsn5b 
 |-  ( ( ph /\ g e. G ) -> ( Y e. ( ._|_ ` ( L ` g ) ) <-> ( N ` { Y } ) C_ ( ._|_ ` ( L ` g ) ) ) )
47 40 43 46 3imtr4d 
 |-  ( ( ph /\ g e. G ) -> ( X e. ( ._|_ ` ( L ` g ) ) -> Y e. ( ._|_ ` ( L ` g ) ) ) )
48 47 imp 
 |-  ( ( ( ph /\ g e. G ) /\ X e. ( ._|_ ` ( L ` g ) ) ) -> Y e. ( ._|_ ` ( L ` g ) ) )
49 4 31 lssvacl 
 |-  ( ( ( U e. LMod /\ ( ._|_ ` ( L ` g ) ) e. ( LSubSp ` U ) ) /\ ( X e. ( ._|_ ` ( L ` g ) ) /\ Y e. ( ._|_ ` ( L ` g ) ) ) ) -> ( X .+ Y ) e. ( ._|_ ` ( L ` g ) ) )
50 20 34 35 48 49 syl22anc 
 |-  ( ( ( ph /\ g e. G ) /\ X e. ( ._|_ ` ( L ` g ) ) ) -> ( X .+ Y ) e. ( ._|_ ` ( L ` g ) ) )
51 50 ex 
 |-  ( ( ph /\ g e. G ) -> ( X e. ( ._|_ ` ( L ` g ) ) -> ( X .+ Y ) e. ( ._|_ ` ( L ` g ) ) ) )
52 51 reximdva 
 |-  ( ph -> ( E. g e. G X e. ( ._|_ ` ( L ` g ) ) -> E. g e. G ( X .+ Y ) e. ( ._|_ ` ( L ` g ) ) ) )
53 17 52 mpd 
 |-  ( ph -> E. g e. G ( X .+ Y ) e. ( ._|_ ` ( L ` g ) ) )
54 eliun 
 |-  ( ( X .+ Y ) e. U_ g e. G ( ._|_ ` ( L ` g ) ) <-> E. g e. G ( X .+ Y ) e. ( ._|_ ` ( L ` g ) ) )
55 53 54 sylibr 
 |-  ( ph -> ( X .+ Y ) e. U_ g e. G ( ._|_ ` ( L ` g ) ) )
56 55 11 eleqtrrdi 
 |-  ( ph -> ( X .+ Y ) e. E )