Metamath Proof Explorer

Theorem lclkrlem2b

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

Ref Expression
Hypotheses lclkrlem2a.h ⊢ H = LHyp ⁡ K
lclkrlem2a.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
lclkrlem2a.u ⊢ U = DVecH ⁡ K ⁡ W
lclkrlem2a.v ⊢ V = Base U
lclkrlem2a.z ⊢ 0 ˙ = 0 U
lclkrlem2a.p ⊢ ⊕ ˙ = LSSum ⁡ U
lclkrlem2a.n ⊢ N = LSpan ⁡ U
lclkrlem2a.a ⊢ A = LSAtoms ⁡ U
lclkrlem2a.k ⊢ φ → K ∈ HL ∧ W ∈ H
lclkrlem2a.b ⊢ φ → B ∈ V ∖ 0 ˙
lclkrlem2a.x ⊢ φ → X ∈ V ∖ 0 ˙
lclkrlem2a.y ⊢ φ → Y ∈ V ∖ 0 ˙
lclkrlem2a.e ⊢ φ → ⊥ ˙ ⁡ X ≠ ⊥ ˙ ⁡ Y
lclkrlem2b.da ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ B ∨ ¬ Y ∈ ⊥ ˙ ⁡ B
Assertion lclkrlem2b ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B ∈ A

Proof

Step Hyp Ref Expression
1 lclkrlem2a.h ⊢ H = LHyp ⁡ K
2 lclkrlem2a.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 lclkrlem2a.u ⊢ U = DVecH ⁡ K ⁡ W
4 lclkrlem2a.v ⊢ V = Base U
5 lclkrlem2a.z ⊢ 0 ˙ = 0 U
6 lclkrlem2a.p ⊢ ⊕ ˙ = LSSum ⁡ U
7 lclkrlem2a.n ⊢ N = LSpan ⁡ U
8 lclkrlem2a.a ⊢ A = LSAtoms ⁡ U
9 lclkrlem2a.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 lclkrlem2a.b ⊢ φ → B ∈ V ∖ 0 ˙
11 lclkrlem2a.x ⊢ φ → X ∈ V ∖ 0 ˙
12 lclkrlem2a.y ⊢ φ → Y ∈ V ∖ 0 ˙
13 lclkrlem2a.e ⊢ φ → ⊥ ˙ ⁡ X ≠ ⊥ ˙ ⁡ Y
14 lclkrlem2b.da ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ B ∨ ¬ Y ∈ ⊥ ˙ ⁡ B
15 9 adantr ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → K ∈ HL ∧ W ∈ H
16 10 adantr ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → B ∈ V ∖ 0 ˙
17 11 adantr ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → X ∈ V ∖ 0 ˙
18 12 adantr ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → Y ∈ V ∖ 0 ˙
19 13 adantr ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → ⊥ ˙ ⁡ X ≠ ⊥ ˙ ⁡ Y
20 simpr ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → ¬ X ∈ ⊥ ˙ ⁡ B
21 1 2 3 4 5 6 7 8 15 16 17 18 19 20 lclkrlem2a ⊢ φ ∧ ¬ X ∈ ⊥ ˙ ⁡ B → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B ∈ A
22 1 3 9 dvhlmod ⊢ φ → U ∈ LMod
23 lmodabl ⊢ U ∈ LMod → U ∈ Abel
24 22 23 syl ⊢ φ → U ∈ Abel
25 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
26 25 lsssssubg ⊢ U ∈ LMod → LSubSp ⁡ U ⊆ SubGrp ⁡ U
27 22 26 syl ⊢ φ → LSubSp ⁡ U ⊆ SubGrp ⁡ U
28 11 eldifad ⊢ φ → X ∈ V
29 4 25 7 lspsncl ⊢ U ∈ LMod ∧ X ∈ V → N ⁡ X ∈ LSubSp ⁡ U
30 22 28 29 syl2anc ⊢ φ → N ⁡ X ∈ LSubSp ⁡ U
31 27 30 sseldd ⊢ φ → N ⁡ X ∈ SubGrp ⁡ U
32 12 eldifad ⊢ φ → Y ∈ V
33 4 25 7 lspsncl ⊢ U ∈ LMod ∧ Y ∈ V → N ⁡ Y ∈ LSubSp ⁡ U
34 22 32 33 syl2anc ⊢ φ → N ⁡ Y ∈ LSubSp ⁡ U
35 27 34 sseldd ⊢ φ → N ⁡ Y ∈ SubGrp ⁡ U
36 6 lsmcom ⊢ U ∈ Abel ∧ N ⁡ X ∈ SubGrp ⁡ U ∧ N ⁡ Y ∈ SubGrp ⁡ U → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ Y ⊕ ˙ N ⁡ X
37 24 31 35 36 syl3anc ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ Y ⊕ ˙ N ⁡ X
38 37 ineq1d ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B = N ⁡ Y ⊕ ˙ N ⁡ X ∩ ⊥ ˙ ⁡ B
39 38 adantr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B = N ⁡ Y ⊕ ˙ N ⁡ X ∩ ⊥ ˙ ⁡ B
40 9 adantr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → K ∈ HL ∧ W ∈ H
41 10 adantr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → B ∈ V ∖ 0 ˙
42 12 adantr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → Y ∈ V ∖ 0 ˙
43 11 adantr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → X ∈ V ∖ 0 ˙
44 13 necomd ⊢ φ → ⊥ ˙ ⁡ Y ≠ ⊥ ˙ ⁡ X
45 44 adantr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → ⊥ ˙ ⁡ Y ≠ ⊥ ˙ ⁡ X
46 simpr ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → ¬ Y ∈ ⊥ ˙ ⁡ B
47 1 2 3 4 5 6 7 8 40 41 42 43 45 46 lclkrlem2a ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → N ⁡ Y ⊕ ˙ N ⁡ X ∩ ⊥ ˙ ⁡ B ∈ A
48 39 47 eqeltrd ⊢ φ ∧ ¬ Y ∈ ⊥ ˙ ⁡ B → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B ∈ A
49 21 48 14 mpjaodan ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B ∈ A