Metamath Proof Explorer

Theorem dihjatcclem2

Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihjatcclem.b ⊢ B = Base K
dihjatcclem.l ⊢ ≤ ˙ = ≤ K
dihjatcclem.h ⊢ H = LHyp ⁡ K
dihjatcclem.j ⊢ ∨ ˙ = join ⁡ K
dihjatcclem.m ⊢ ∧ ˙ = meet ⁡ K
dihjatcclem.a ⊢ A = Atoms ⁡ K
dihjatcclem.u ⊢ U = DVecH ⁡ K ⁡ W
dihjatcclem.s ⊢ ⊕ ˙ = LSSum ⁡ U
dihjatcclem.i ⊢ I = DIsoH ⁡ K ⁡ W
dihjatcclem.v ⊢ V = P ∨ ˙ Q ∧ ˙ W
dihjatcclem.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihjatcclem.p ⊢ φ → P ∈ A ∧ ¬ P ≤ ˙ W
dihjatcclem.q ⊢ φ → Q ∈ A ∧ ¬ Q ≤ ˙ W
dihjatcclem2.c ⊢ φ → I ⁡ V ⊆ I ⁡ P ⊕ ˙ I ⁡ Q
Assertion dihjatcclem2 ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q

Proof

Step Hyp Ref Expression
1 dihjatcclem.b ⊢ B = Base K
2 dihjatcclem.l ⊢ ≤ ˙ = ≤ K
3 dihjatcclem.h ⊢ H = LHyp ⁡ K
4 dihjatcclem.j ⊢ ∨ ˙ = join ⁡ K
5 dihjatcclem.m ⊢ ∧ ˙ = meet ⁡ K
6 dihjatcclem.a ⊢ A = Atoms ⁡ K
7 dihjatcclem.u ⊢ U = DVecH ⁡ K ⁡ W
8 dihjatcclem.s ⊢ ⊕ ˙ = LSSum ⁡ U
9 dihjatcclem.i ⊢ I = DIsoH ⁡ K ⁡ W
10 dihjatcclem.v ⊢ V = P ∨ ˙ Q ∧ ˙ W
11 dihjatcclem.k ⊢ φ → K ∈ HL ∧ W ∈ H
12 dihjatcclem.p ⊢ φ → P ∈ A ∧ ¬ P ≤ ˙ W
13 dihjatcclem.q ⊢ φ → Q ∈ A ∧ ¬ Q ≤ ˙ W
14 dihjatcclem2.c ⊢ φ → I ⁡ V ⊆ I ⁡ P ⊕ ˙ I ⁡ Q
15 1 2 3 4 5 6 7 8 9 10 11 12 13 dihjatcclem1 ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V
16 3 7 11 dvhlmod ⊢ φ → U ∈ LMod
17 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
18 17 lsssssubg ⊢ U ∈ LMod → LSubSp ⁡ U ⊆ SubGrp ⁡ U
19 16 18 syl ⊢ φ → LSubSp ⁡ U ⊆ SubGrp ⁡ U
20 12 simpld ⊢ φ → P ∈ A
21 1 6 atbase ⊢ P ∈ A → P ∈ B
22 20 21 syl ⊢ φ → P ∈ B
23 1 3 9 7 17 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ B → I ⁡ P ∈ LSubSp ⁡ U
24 11 22 23 syl2anc ⊢ φ → I ⁡ P ∈ LSubSp ⁡ U
25 13 simpld ⊢ φ → Q ∈ A
26 1 6 atbase ⊢ Q ∈ A → Q ∈ B
27 25 26 syl ⊢ φ → Q ∈ B
28 1 3 9 7 17 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ B → I ⁡ Q ∈ LSubSp ⁡ U
29 11 27 28 syl2anc ⊢ φ → I ⁡ Q ∈ LSubSp ⁡ U
30 17 8 lsmcl ⊢ U ∈ LMod ∧ I ⁡ P ∈ LSubSp ⁡ U ∧ I ⁡ Q ∈ LSubSp ⁡ U → I ⁡ P ⊕ ˙ I ⁡ Q ∈ LSubSp ⁡ U
31 16 24 29 30 syl3anc ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ Q ∈ LSubSp ⁡ U
32 19 31 sseldd ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ Q ∈ SubGrp ⁡ U
33 10 fveq2i ⊢ I ⁡ V = I ⁡ P ∨ ˙ Q ∧ ˙ W
34 11 simpld ⊢ φ → K ∈ HL
35 34 hllatd ⊢ φ → K ∈ Lat
36 1 4 6 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ B
37 34 20 25 36 syl3anc ⊢ φ → P ∨ ˙ Q ∈ B
38 11 simprd ⊢ φ → W ∈ H
39 1 3 lhpbase ⊢ W ∈ H → W ∈ B
40 38 39 syl ⊢ φ → W ∈ B
41 1 5 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ B ∧ W ∈ B → P ∨ ˙ Q ∧ ˙ W ∈ B
42 35 37 40 41 syl3anc ⊢ φ → P ∨ ˙ Q ∧ ˙ W ∈ B
43 1 3 9 7 17 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ Q ∧ ˙ W ∈ B → I ⁡ P ∨ ˙ Q ∧ ˙ W ∈ LSubSp ⁡ U
44 11 42 43 syl2anc ⊢ φ → I ⁡ P ∨ ˙ Q ∧ ˙ W ∈ LSubSp ⁡ U
45 33 44 eqeltrid ⊢ φ → I ⁡ V ∈ LSubSp ⁡ U
46 19 45 sseldd ⊢ φ → I ⁡ V ∈ SubGrp ⁡ U
47 8 lsmss2 ⊢ I ⁡ P ⊕ ˙ I ⁡ Q ∈ SubGrp ⁡ U ∧ I ⁡ V ∈ SubGrp ⁡ U ∧ I ⁡ V ⊆ I ⁡ P ⊕ ˙ I ⁡ Q → I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V = I ⁡ P ⊕ ˙ I ⁡ Q
48 32 46 14 47 syl3anc ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V = I ⁡ P ⊕ ˙ I ⁡ Q
49 15 48 eqtrd ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q