Metamath Proof Explorer

Theorem lclkrlem2d

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
lclkrlem2d.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion lclkrlem2d ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ⊕ ˙ N ⁡ B ∈ ran ⁡ I

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 lclkrlem2d.i ⊢ I = DIsoH ⁡ K ⁡ W
16 11 eldifad ⊢ φ → X ∈ V
17 16 snssd ⊢ φ → X ⊆ V
18 1 15 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ I
19 9 17 18 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ ran ⁡ I
20 12 eldifad ⊢ φ → Y ∈ V
21 20 snssd ⊢ φ → Y ⊆ V
22 1 15 3 4 2 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ⊆ V → ⊥ ˙ ⁡ Y ∈ ran ⁡ I
23 9 21 22 syl2anc ⊢ φ → ⊥ ˙ ⁡ Y ∈ ran ⁡ I
24 1 15 dihmeetcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ I ∧ ⊥ ˙ ⁡ Y ∈ ran ⁡ I → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ∈ ran ⁡ I
25 9 19 23 24 syl12anc ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ∈ ran ⁡ I
26 10 eldifad ⊢ φ → B ∈ V
27 1 3 4 6 7 15 9 25 26 dihsmsprn ⊢ φ → ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ Y ⊕ ˙ N ⁡ B ∈ ran ⁡ I