Metamath Proof Explorer

Theorem lclkrlem2s

Description: Lemma for lclkr . Thus, the sum has a closed kernel when B is zero. (Contributed by NM, 18-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 } ) )
lclkrlem2q.b 
|- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )
lclkrlem2q.n 
|- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )
lclkrlem2r.bn 
|- ( ph -> B = ( 0g ` U ) )
Assertion lclkrlem2s 
|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )

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 lclkrlem2q.b 
 |-  B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) )
25 lclkrlem2q.n 
 |-  ( ph -> ( ( E .+ G ) ` Y ) =/= .0. )
26 lclkrlem2r.bn 
 |-  ( ph -> B = ( 0g ` U ) )
27 12 snssd 
 |-  ( ph -> { Y } C_ V )
28 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
29 17 28 19 1 18 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { Y } C_ V ) -> ( ._|_ ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
30 21 27 29 syl2anc 
 |-  ( ph -> ( ._|_ ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
31 17 28 18 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { Y } ) ) ) = ( ._|_ ` { Y } ) )
32 21 30 31 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { Y } ) ) ) = ( ._|_ ` { Y } ) )
33 32 ad2antrr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { Y } ) ) ) = ( ._|_ ` { Y } ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 lclkrlem2r 
 |-  ( ph -> ( L ` G ) C_ ( L ` ( E .+ G ) ) )
35 34 ad2antrr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` G ) C_ ( L ` ( E .+ G ) ) )
36 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
37 17 19 21 dvhlvec 
 |-  ( ph -> U e. LVec )
38 37 ad2antrr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> U e. LVec )
39 simplr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` G ) e. ( LSHyp ` U ) )
40 simpr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) )
41 36 38 39 40 lshpcmp 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ( L ` G ) C_ ( L ` ( E .+ G ) ) <-> ( L ` G ) = ( L ` ( E .+ G ) ) ) )
42 35 41 mpbid 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` G ) = ( L ` ( E .+ G ) ) )
43 23 ad2antrr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` G ) = ( ._|_ ` { Y } ) )
44 42 43 eqtr3d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` ( E .+ G ) ) = ( ._|_ ` { Y } ) )
45 44 fveq2d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( L ` ( E .+ G ) ) ) = ( ._|_ ` ( ._|_ ` { Y } ) ) )
46 45 fveq2d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( ._|_ ` ( ._|_ ` ( ._|_ ` { Y } ) ) ) )
47 33 46 44 3eqtr4d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
48 17 19 18 1 21 dochoc1 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )
49 48 ad2antrr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) = V ) -> ( ._|_ ` ( ._|_ ` V ) ) = V )
50 simpr 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) = V ) -> ( L ` ( E .+ G ) ) = V )
51 50 fveq2d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) = V ) -> ( ._|_ ` ( L ` ( E .+ G ) ) ) = ( ._|_ ` V ) )
52 51 fveq2d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
53 49 52 50 3eqtr4d 
 |-  ( ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) /\ ( L ` ( E .+ G ) ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
54 17 19 21 dvhlmod 
 |-  ( ph -> U e. LMod )
55 8 9 10 54 13 14 ldualvaddcl 
 |-  ( ph -> ( E .+ G ) e. F )
56 1 36 8 16 37 55 lkrshpor 
 |-  ( ph -> ( ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) \/ ( L ` ( E .+ G ) ) = V ) )
57 56 adantr 
 |-  ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) -> ( ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) \/ ( L ` ( E .+ G ) ) = V ) )
58 47 53 57 mpjaodan 
 |-  ( ( ph /\ ( L ` G ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
59 48 adantr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` V ) ) = V )
60 1 8 16 54 55 lkrssv 
 |-  ( ph -> ( L ` ( E .+ G ) ) C_ V )
61 60 adantr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( L ` ( E .+ G ) ) C_ V )
62 simpr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( L ` G ) = V )
63 34 adantr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( L ` G ) C_ ( L ` ( E .+ G ) ) )
64 62 63 eqsstrrd 
 |-  ( ( ph /\ ( L ` G ) = V ) -> V C_ ( L ` ( E .+ G ) ) )
65 61 64 eqssd 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( L ` ( E .+ G ) ) = V )
66 65 fveq2d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( L ` ( E .+ G ) ) ) = ( ._|_ ` V ) )
67 66 fveq2d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
68 59 67 65 3eqtr4d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
69 1 36 8 16 37 14 lkrshpor 
 |-  ( ph -> ( ( L ` G ) e. ( LSHyp ` U ) \/ ( L ` G ) = V ) )
70 58 68 69 mpjaodan 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )