Metamath Proof Explorer

Theorem lclkrlem2b

Description: Lemma for lclkr . (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2a.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2a.z ⊢ 0 = ( 0g ‘ 𝑈 )
lclkrlem2a.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
lclkrlem2a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2a.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
lclkrlem2a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2a.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2a.e ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
lclkrlem2b.da ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
Assertion lclkrlem2b ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 lclkrlem2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrlem2a.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrlem2a.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2a.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lclkrlem2a.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 lclkrlem2a.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
7 lclkrlem2a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 lclkrlem2a.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lclkrlem2a.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lclkrlem2a.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
11 lclkrlem2a.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12 lclkrlem2a.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
13 lclkrlem2a.e ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
14 lclkrlem2b.da ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
15 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
17 11 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
18 12 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
19 13 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
20 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) )
21 1 2 3 4 5 6 7 8 15 16 17 18 19 20 lclkrlem2a ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )
22 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
23 lmodabl ⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Abel )
24 22 23 syl ⊢ ( 𝜑 → 𝑈 ∈ Abel )
25 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
26 25 lsssssubg ⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
27 22 26 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
28 11 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
29 4 25 7 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
30 22 28 29 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
31 27 30 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑈 ) )
32 12 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
33 4 25 7 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
34 22 32 33 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
35 27 34 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑈 ) )
36 6 lsmcom ⊢ ( ( 𝑈 ∈ Abel ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
37 24 31 35 36 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
38 37 ineq1d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) )
40 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
41 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
42 12 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
43 11 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
44 13 necomd ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑌 } ) ≠ ( ⊥ ‘ { 𝑋 } ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( ⊥ ‘ { 𝑌 } ) ≠ ( ⊥ ‘ { 𝑋 } ) )
46 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) )
47 1 2 3 4 5 6 7 8 40 41 42 43 45 46 lclkrlem2a ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )
48 39 47 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )
49 21 48 14 mpjaodan ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )