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 ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2o.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2o.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
lclkrlem2o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2q.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
lclkrlem2q.lg ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
lclkrlem2q.b ⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
lclkrlem2q.n ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
lclkrlem2r.bn ⊢ ( 𝜑 → 𝐵 = ( 0g ‘ 𝑈 ) )
Assertion lclkrlem2s ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
2 lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
3 lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
5 lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
7 lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
8 lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
10 lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
11 lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14 lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15 lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
16 lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
17 lclkrlem2o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
18 lclkrlem2o.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
19 lclkrlem2o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
20 lclkrlem2o.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
21 lclkrlem2o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22 lclkrlem2q.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
23 lclkrlem2q.lg ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
24 lclkrlem2q.b ⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
25 lclkrlem2q.n ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
26 lclkrlem2r.bn ⊢ ( 𝜑 → 𝐵 = ( 0g ‘ 𝑈 ) )
27 12 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
28 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
29 17 28 19 1 18 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑌 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
30 21 27 29 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
31 17 28 18 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) ) = ( ⊥ ‘ { 𝑌 } ) )
32 21 30 31 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) ) = ( ⊥ ‘ { 𝑌 } ) )
33 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) ) = ( ⊥ ‘ { 𝑌 } ) )
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 ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
35 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
36 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
37 17 19 21 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → 𝑈 ∈ LVec )
39 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) )
41 36 38 39 40 lshpcmp ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ↔ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
42 35 41 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
43 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
44 42 43 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = ( ⊥ ‘ { 𝑌 } ) )
45 44 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑌 } ) ) ) )
47 33 46 44 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
48 17 19 18 1 21 dochoc1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
50 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 )
51 50 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) = ( ⊥ ‘ 𝑉 ) )
52 51 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
53 49 52 50 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
54 17 19 21 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
55 8 9 10 54 13 14 ldualvaddcl ⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
56 1 36 8 16 37 55 lkrshpor ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ∨ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ∨ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) )
58 47 53 57 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
59 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
60 1 8 16 54 55 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ 𝑉 )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ 𝑉 )
62 simpr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
63 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
64 62 63 eqsstrrd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → 𝑉 ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
65 61 64 eqssd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 )
66 65 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) = ( ⊥ ‘ 𝑉 ) )
67 66 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
68 59 67 65 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
69 1 36 8 16 37 14 lkrshpor ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
70 58 68 69 mpjaodan ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )