Metamath Proof Explorer

Theorem lclkrlem2c

Description: Lemma for lclkr . (Contributed by NM, 16-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
lclkrlem2c.j ⊢ J = LSHyp ⁡ U
Assertion lclkrlem2c ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ⊕ ˙ N ⁡ B ∈ J

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 lclkrlem2c.j ⊢ J = LSHyp ⁡ U
16 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
17 eqid ⊢ joinH ⁡ K ⁡ W = joinH ⁡ K ⁡ W
18 11 eldifad ⊢ φ → X ∈ V
19 1 3 4 7 16 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ V → N ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
20 9 18 19 syl2anc ⊢ φ → N ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
21 1 3 9 dvhlmod ⊢ φ → U ∈ LMod
22 4 7 5 8 21 12 lsatlspsn ⊢ φ → N ⁡ Y ∈ A
23 1 16 3 6 8 9 20 22 dihsmatrn ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
24 10 eldifad ⊢ φ → B ∈ V
25 24 snssd ⊢ φ → B ⊆ V
26 1 16 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ B ⊆ V → ⊥ ˙ ⁡ B ∈ ran ⁡ DIsoH ⁡ K ⁡ W
27 9 25 26 syl2anc ⊢ φ → ⊥ ˙ ⁡ B ∈ ran ⁡ DIsoH ⁡ K ⁡ W
28 1 16 3 4 2 17 9 23 27 dochdmm1 ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B = ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y joinH ⁡ K ⁡ W ⊥ ˙ ⁡ ⊥ ˙ ⁡ B
29 12 eldifad ⊢ φ → Y ∈ V
30 4 7 6 21 18 29 lsmpr ⊢ φ → N ⁡ X Y = N ⁡ X ⊕ ˙ N ⁡ Y
31 df-pr ⊢ X Y = X ∪ Y
32 31 fveq2i ⊢ N ⁡ X Y = N ⁡ X ∪ Y
33 30 32 eqtr3di ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X ∪ Y
34 33 fveq2d ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y = ⊥ ˙ ⁡ N ⁡ X ∪ Y
35 18 snssd ⊢ φ → X ⊆ V
36 29 snssd ⊢ φ → Y ⊆ V
37 35 36 unssd ⊢ φ → X ∪ Y ⊆ V
38 1 3 2 4 7 9 37 dochocsp ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ∪ Y = ⊥ ˙ ⁡ X ∪ Y
39 1 3 4 2 dochdmj1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → ⊥ ˙ ⁡ X ∪ Y = ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
40 9 35 36 39 syl3anc ⊢ φ → ⊥ ˙ ⁡ X ∪ Y = ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
41 34 38 40 3eqtrd ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y = ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y
42 1 3 2 4 7 9 24 dochocsn ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ B = N ⁡ B
43 41 42 oveq12d ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y joinH ⁡ K ⁡ W ⊥ ˙ ⁡ ⊥ ˙ ⁡ B = ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y joinH ⁡ K ⁡ W N ⁡ B
44 1 16 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
45 9 35 44 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
46 1 16 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ⊆ V → ⊥ ˙ ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
47 9 36 46 syl2anc ⊢ φ → ⊥ ˙ ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
48 1 16 dihmeetcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W ∧ ⊥ ˙ ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
49 9 45 47 48 syl12anc ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ∈ ran ⁡ DIsoH ⁡ K ⁡ W
50 1 3 4 6 7 16 17 9 49 24 dihjat1 ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y joinH ⁡ K ⁡ W N ⁡ B = ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ⊕ ˙ N ⁡ B
51 28 43 50 3eqtrrd ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ⊕ ˙ N ⁡ B = ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B
52 1 2 3 4 5 6 7 8 9 10 11 12 13 14 lclkrlem2b ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B ∈ A
53 1 3 2 8 15 9 52 dochsatshp ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ⊕ ˙ N ⁡ Y ∩ ⊥ ˙ ⁡ B ∈ J
54 51 53 eqeltrd ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ⊕ ˙ N ⁡ B ∈ J