Metamath Proof Explorer

Theorem dihjatcclem1

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
Assertion dihjatcclem1 ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V

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 3 7 11 dvhlmod ⊢ φ → U ∈ LMod
15 lmodabl ⊢ U ∈ LMod → U ∈ Abel
16 14 15 syl ⊢ φ → U ∈ Abel
17 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
18 17 lsssssubg ⊢ U ∈ LMod → LSubSp ⁡ U ⊆ SubGrp ⁡ U
19 14 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 19 24 sseldd ⊢ φ → I ⁡ P ∈ SubGrp ⁡ U
26 11 simpld ⊢ φ → K ∈ HL
27 26 hllatd ⊢ φ → K ∈ Lat
28 13 simpld ⊢ φ → Q ∈ A
29 1 4 6 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ B
30 26 20 28 29 syl3anc ⊢ φ → P ∨ ˙ Q ∈ B
31 11 simprd ⊢ φ → W ∈ H
32 1 3 lhpbase ⊢ W ∈ H → W ∈ B
33 31 32 syl ⊢ φ → W ∈ B
34 1 5 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ B ∧ W ∈ B → P ∨ ˙ Q ∧ ˙ W ∈ B
35 27 30 33 34 syl3anc ⊢ φ → P ∨ ˙ Q ∧ ˙ W ∈ B
36 10 35 eqeltrid ⊢ φ → V ∈ B
37 1 3 9 7 17 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ B → I ⁡ V ∈ LSubSp ⁡ U
38 11 36 37 syl2anc ⊢ φ → I ⁡ V ∈ LSubSp ⁡ U
39 19 38 sseldd ⊢ φ → I ⁡ V ∈ SubGrp ⁡ U
40 1 6 atbase ⊢ Q ∈ A → Q ∈ B
41 28 40 syl ⊢ φ → Q ∈ B
42 1 3 9 7 17 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ B → I ⁡ Q ∈ LSubSp ⁡ U
43 11 41 42 syl2anc ⊢ φ → I ⁡ Q ∈ LSubSp ⁡ U
44 19 43 sseldd ⊢ φ → I ⁡ Q ∈ SubGrp ⁡ U
45 8 lsm4 ⊢ U ∈ Abel ∧ I ⁡ P ∈ SubGrp ⁡ U ∧ I ⁡ V ∈ SubGrp ⁡ U ∧ I ⁡ Q ∈ SubGrp ⁡ U ∧ I ⁡ V ∈ SubGrp ⁡ U → I ⁡ P ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V = I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ V
46 16 25 39 44 39 45 syl122anc ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V = I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ V
47 13 simprd ⊢ φ → ¬ Q ≤ ˙ W
48 47 intnand ⊢ φ → ¬ P ≤ ˙ W ∧ Q ≤ ˙ W
49 1 2 4 latjle12 ⊢ K ∈ Lat ∧ P ∈ B ∧ Q ∈ B ∧ W ∈ B → P ≤ ˙ W ∧ Q ≤ ˙ W ↔ P ∨ ˙ Q ≤ ˙ W
50 27 22 41 33 49 syl13anc ⊢ φ → P ≤ ˙ W ∧ Q ≤ ˙ W ↔ P ∨ ˙ Q ≤ ˙ W
51 48 50 mtbid ⊢ φ → ¬ P ∨ ˙ Q ≤ ˙ W
52 2 4 6 hlatlej1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≤ ˙ P ∨ ˙ Q
53 26 20 28 52 syl3anc ⊢ φ → P ≤ ˙ P ∨ ˙ Q
54 1 2 4 5 6 3 9 7 8 dihvalcq2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ Q ∈ B ∧ ¬ P ∨ ˙ Q ≤ ˙ W ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ P ≤ ˙ P ∨ ˙ Q → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ P ∨ ˙ Q ∧ ˙ W
55 11 30 51 12 53 54 syl122anc ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ P ∨ ˙ Q ∧ ˙ W
56 10 fveq2i ⊢ I ⁡ V = I ⁡ P ∨ ˙ Q ∧ ˙ W
57 56 oveq2i ⊢ I ⁡ P ⊕ ˙ I ⁡ V = I ⁡ P ⊕ ˙ I ⁡ P ∨ ˙ Q ∧ ˙ W
58 55 57 eqtr4di ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ V
59 2 4 6 hlatlej2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → Q ≤ ˙ P ∨ ˙ Q
60 26 20 28 59 syl3anc ⊢ φ → Q ≤ ˙ P ∨ ˙ Q
61 1 2 4 5 6 3 9 7 8 dihvalcq2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ Q ∈ B ∧ ¬ P ∨ ˙ Q ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ Q ≤ ˙ P ∨ ˙ Q → I ⁡ P ∨ ˙ Q = I ⁡ Q ⊕ ˙ I ⁡ P ∨ ˙ Q ∧ ˙ W
62 11 30 51 13 60 61 syl122anc ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ Q ⊕ ˙ I ⁡ P ∨ ˙ Q ∧ ˙ W
63 56 oveq2i ⊢ I ⁡ Q ⊕ ˙ I ⁡ V = I ⁡ Q ⊕ ˙ I ⁡ P ∨ ˙ Q ∧ ˙ W
64 62 63 eqtr4di ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ Q ⊕ ˙ I ⁡ V
65 58 64 oveq12d ⊢ φ → I ⁡ P ∨ ˙ Q ⊕ ˙ I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V
66 1 3 9 7 17 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ P ∨ ˙ Q ∈ B → I ⁡ P ∨ ˙ Q ∈ LSubSp ⁡ U
67 11 30 66 syl2anc ⊢ φ → I ⁡ P ∨ ˙ Q ∈ LSubSp ⁡ U
68 19 67 sseldd ⊢ φ → I ⁡ P ∨ ˙ Q ∈ SubGrp ⁡ U
69 8 lsmidm ⊢ I ⁡ P ∨ ˙ Q ∈ SubGrp ⁡ U → I ⁡ P ∨ ˙ Q ⊕ ˙ I ⁡ P ∨ ˙ Q = I ⁡ P ∨ ˙ Q
70 68 69 syl ⊢ φ → I ⁡ P ∨ ˙ Q ⊕ ˙ I ⁡ P ∨ ˙ Q = I ⁡ P ∨ ˙ Q
71 65 70 eqtr3d ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V = I ⁡ P ∨ ˙ Q
72 8 lsmidm ⊢ I ⁡ V ∈ SubGrp ⁡ U → I ⁡ V ⊕ ˙ I ⁡ V = I ⁡ V
73 39 72 syl ⊢ φ → I ⁡ V ⊕ ˙ I ⁡ V = I ⁡ V
74 73 oveq2d ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V ⊕ ˙ I ⁡ V = I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V
75 46 71 74 3eqtr3d ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q ⊕ ˙ I ⁡ V