Metamath Proof Explorer

Theorem lclkrlem2v

Description: Lemma for lclkr . When the hypotheses of lclkrlem2u and lclkrlem2u are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid , which requires the orthomodular law dihoml4 (Lemma 3.3 of Holland95 p. 214). (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v 
|- V = ( Base ` U )
lclkrlem2m.t 
|- .x. = ( .s ` U )
lclkrlem2m.s 
|- S = ( Scalar ` U )
lclkrlem2m.q 
|- .X. = ( .r ` S )
lclkrlem2m.z 
|- .0. = ( 0g ` S )
lclkrlem2m.i 
|- I = ( invr ` S )
lclkrlem2m.m 
|- .- = ( -g ` U )
lclkrlem2m.f 
|- F = ( LFnl ` U )
lclkrlem2m.d 
|- D = ( LDual ` U )
lclkrlem2m.p 
|- .+ = ( +g ` D )
lclkrlem2m.x 
|- ( ph -> X e. V )
lclkrlem2m.y 
|- ( ph -> Y e. V )
lclkrlem2m.e 
|- ( ph -> E e. F )
lclkrlem2m.g 
|- ( ph -> G e. F )
lclkrlem2n.n 
|- N = ( LSpan ` U )
lclkrlem2n.l 
|- L = ( LKer ` U )
lclkrlem2o.h 
|- H = ( LHyp ` K )
lclkrlem2o.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem2o.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrlem2o.a 
|- .(+) = ( LSSum ` U )
lclkrlem2o.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem2q.le 
|- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
lclkrlem2q.lg 
|- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
lclkrlem2v.j 
|- ( ph -> ( ( E .+ G ) ` X ) = .0. )
lclkrlem2v.k 
|- ( ph -> ( ( E .+ G ) ` Y ) = .0. )
Assertion lclkrlem2v 
|- ( ph -> ( L ` ( E .+ G ) ) = V )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v 
 |-  V = ( Base ` U )
2 lclkrlem2m.t 
 |-  .x. = ( .s ` U )
3 lclkrlem2m.s 
 |-  S = ( Scalar ` U )
4 lclkrlem2m.q 
 |-  .X. = ( .r ` S )
5 lclkrlem2m.z 
 |-  .0. = ( 0g ` S )
6 lclkrlem2m.i 
 |-  I = ( invr ` S )
7 lclkrlem2m.m 
 |-  .- = ( -g ` U )
8 lclkrlem2m.f 
 |-  F = ( LFnl ` U )
9 lclkrlem2m.d 
 |-  D = ( LDual ` U )
10 lclkrlem2m.p 
 |-  .+ = ( +g ` D )
11 lclkrlem2m.x 
 |-  ( ph -> X e. V )
12 lclkrlem2m.y 
 |-  ( ph -> Y e. V )
13 lclkrlem2m.e 
 |-  ( ph -> E e. F )
14 lclkrlem2m.g 
 |-  ( ph -> G e. F )
15 lclkrlem2n.n 
 |-  N = ( LSpan ` U )
16 lclkrlem2n.l 
 |-  L = ( LKer ` U )
17 lclkrlem2o.h 
 |-  H = ( LHyp ` K )
18 lclkrlem2o.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
19 lclkrlem2o.u 
 |-  U = ( ( DVecH ` K ) ` W )
20 lclkrlem2o.a 
 |-  .(+) = ( LSSum ` U )
21 lclkrlem2o.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
22 lclkrlem2q.le 
 |-  ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
23 lclkrlem2q.lg 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
24 lclkrlem2v.j 
 |-  ( ph -> ( ( E .+ G ) ` X ) = .0. )
25 lclkrlem2v.k 
 |-  ( ph -> ( ( E .+ G ) ` Y ) = .0. )
26 17 19 21 dvhlmod 
 |-  ( ph -> U e. LMod )
27 8 9 10 26 13 14 ldualvaddcl 
 |-  ( ph -> ( E .+ G ) e. F )
28 1 8 16 26 27 lkrssv 
 |-  ( ph -> ( L ` ( E .+ G ) ) C_ V )
29 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
30 1 29 15 26 11 12 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
31 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
32 17 19 1 15 31 21 11 12 dihprrn 
 |-  ( ph -> ( N ` { X , Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
33 1 29 lssss 
 |-  ( ( N ` { X , Y } ) e. ( LSubSp ` U ) -> ( N ` { X , Y } ) C_ V )
34 30 33 syl 
 |-  ( ph -> ( N ` { X , Y } ) C_ V )
35 17 31 19 1 18 21 34 dochoccl 
 |-  ( ph -> ( ( N ` { X , Y } ) e. ran ( ( DIsoH ` K ) ` W ) <-> ( ._|_ ` ( ._|_ ` ( N ` { X , Y } ) ) ) = ( N ` { X , Y } ) ) )
36 32 35 mpbid 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( N ` { X , Y } ) ) ) = ( N ` { X , Y } ) )
37 17 18 19 1 29 20 21 30 36 dochexmid 
 |-  ( ph -> ( ( N ` { X , Y } ) .(+) ( ._|_ ` ( N ` { X , Y } ) ) ) = V )
38 17 19 21 dvhlvec 
 |-  ( ph -> U e. LVec )
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 38 24 25 lclkrlem2n 
 |-  ( ph -> ( N ` { X , Y } ) C_ ( L ` ( E .+ G ) ) )
40 11 snssd 
 |-  ( ph -> { X } C_ V )
41 12 snssd 
 |-  ( ph -> { Y } C_ V )
42 17 19 1 18 dochdmj1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V /\ { Y } C_ V ) -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
43 21 40 41 42 syl3anc 
 |-  ( ph -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
44 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
45 44 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
46 45 fveq2i 
 |-  ( ._|_ ` ( N ` { X , Y } ) ) = ( ._|_ ` ( N ` ( { X } u. { Y } ) ) )
47 40 41 unssd 
 |-  ( ph -> ( { X } u. { Y } ) C_ V )
48 17 19 18 1 15 21 47 dochocsp 
 |-  ( ph -> ( ._|_ ` ( N ` ( { X } u. { Y } ) ) ) = ( ._|_ ` ( { X } u. { Y } ) ) )
49 46 48 syl5eq 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) = ( ._|_ ` ( { X } u. { Y } ) ) )
50 22 23 ineq12d 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
51 43 49 50 3eqtr4d 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) = ( ( L ` E ) i^i ( L ` G ) ) )
52 8 16 9 10 26 13 14 lkrin 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` ( E .+ G ) ) )
53 51 52 eqsstrd 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) C_ ( L ` ( E .+ G ) ) )
54 29 lsssssubg 
 |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
55 26 54 syl 
 |-  ( ph -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
56 55 30 sseldd 
 |-  ( ph -> ( N ` { X , Y } ) e. ( SubGrp ` U ) )
57 17 19 1 29 18 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X , Y } ) C_ V ) -> ( ._|_ ` ( N ` { X , Y } ) ) e. ( LSubSp ` U ) )
58 21 34 57 syl2anc 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) e. ( LSubSp ` U ) )
59 55 58 sseldd 
 |-  ( ph -> ( ._|_ ` ( N ` { X , Y } ) ) e. ( SubGrp ` U ) )
60 8 16 29 lkrlss 
 |-  ( ( U e. LMod /\ ( E .+ G ) e. F ) -> ( L ` ( E .+ G ) ) e. ( LSubSp ` U ) )
61 26 27 60 syl2anc 
 |-  ( ph -> ( L ` ( E .+ G ) ) e. ( LSubSp ` U ) )
62 55 61 sseldd 
 |-  ( ph -> ( L ` ( E .+ G ) ) e. ( SubGrp ` U ) )
63 20 lsmlub 
 |-  ( ( ( N ` { X , Y } ) e. ( SubGrp ` U ) /\ ( ._|_ ` ( N ` { X , Y } ) ) e. ( SubGrp ` U ) /\ ( L ` ( E .+ G ) ) e. ( SubGrp ` U ) ) -> ( ( ( N ` { X , Y } ) C_ ( L ` ( E .+ G ) ) /\ ( ._|_ ` ( N ` { X , Y } ) ) C_ ( L ` ( E .+ G ) ) ) <-> ( ( N ` { X , Y } ) .(+) ( ._|_ ` ( N ` { X , Y } ) ) ) C_ ( L ` ( E .+ G ) ) ) )
64 56 59 62 63 syl3anc 
 |-  ( ph -> ( ( ( N ` { X , Y } ) C_ ( L ` ( E .+ G ) ) /\ ( ._|_ ` ( N ` { X , Y } ) ) C_ ( L ` ( E .+ G ) ) ) <-> ( ( N ` { X , Y } ) .(+) ( ._|_ ` ( N ` { X , Y } ) ) ) C_ ( L ` ( E .+ G ) ) ) )
65 39 53 64 mpbi2and 
 |-  ( ph -> ( ( N ` { X , Y } ) .(+) ( ._|_ ` ( N ` { X , Y } ) ) ) C_ ( L ` ( E .+ G ) ) )
66 37 65 eqsstrrd 
 |-  ( ph -> V C_ ( L ` ( E .+ G ) ) )
67 28 66 eqssd 
 |-  ( ph -> ( L ` ( E .+ G ) ) = V )