Metamath Proof Explorer

Theorem lclkrlem2e

Description: Lemma for lclkr . The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2e.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2e.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2e.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2e.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2e.z ⊢ 0 = ( 0g ‘ 𝑈 )
lclkrlem2e.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2e.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2e.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2e.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2e.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2e.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2e.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2e.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2e.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
lclkrlem2e.ne ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( 𝐿 ‘ 𝐺 ) )
Assertion lclkrlem2e ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2e.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrlem2e.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrlem2e.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2e.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lclkrlem2e.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 lclkrlem2e.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 lclkrlem2e.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 lclkrlem2e.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
9 lclkrlem2e.p ⊢ + = ( +g ‘ 𝐷 )
10 lclkrlem2e.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 lclkrlem2e.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12 lclkrlem2e.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
13 lclkrlem2e.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
14 lclkrlem2e.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
15 lclkrlem2e.ne ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( 𝐿 ‘ 𝐺 ) )
16 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 11 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
18 17 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → { 𝑋 } ⊆ 𝑉 )
20 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
21 1 20 3 4 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
22 16 19 21 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
23 1 20 2 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ { 𝑋 } ) )
24 16 22 23 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ { 𝑋 } ) )
25 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
26 inidm ⊢ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐸 ) ) = ( 𝐿 ‘ 𝐸 )
27 15 ineq2d ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐸 ) ) = ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) )
28 26 27 eqtr3id ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) )
29 1 3 10 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
30 6 7 8 9 29 12 13 lkrin ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
31 28 30 eqsstrd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐸 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
33 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
34 1 3 10 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → 𝑈 ∈ LVec )
36 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
37 1 3 2 4 36 10 18 dochocsp ⊢ ( 𝜑 → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
39 25 38 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
40 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
41 4 36 5 40 29 11 lsatlspsn ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
43 1 3 2 40 33 16 42 dochsatshp ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ∈ ( LSHyp ‘ 𝑈 ) )
44 39 43 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐸 ) ∈ ( LSHyp ‘ 𝑈 ) )
45 simpr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) )
46 33 35 44 45 lshpcmp ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ( 𝐿 ‘ 𝐸 ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ↔ ( 𝐿 ‘ 𝐸 ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
47 32 46 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐸 ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
48 25 47 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ { 𝑋 } ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
49 48 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) = ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
50 49 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) )
51 24 50 48 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
52 51 ex ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
53 1 3 2 4 10 dochoc1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
54 2fveq3 ⊢ ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
55 id ⊢ ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 )
56 54 55 eqeq12d ⊢ ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 ) )
57 53 56 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) )
58 6 8 9 29 12 13 ldualvaddcl ⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
59 4 33 6 7 34 58 lkrshpor ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSHyp ‘ 𝑈 ) ∨ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) )
60 52 57 59 mpjaod ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )