Metamath Proof Explorer

Theorem dihjat3

Description: Isomorphism H of lattice join with an atom. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dihjat3.b ⊢ B = Base K
dihjat3.h ⊢ H = LHyp ⁡ K
dihjat3.j ⊢ ∨ ˙ = join ⁡ K
dihjat3.a ⊢ A = Atoms ⁡ K
dihjat3.u ⊢ U = DVecH ⁡ K ⁡ W
dihjat3.s ⊢ ⊕ ˙ = LSSum ⁡ U
dihjat3.i ⊢ I = DIsoH ⁡ K ⁡ W
dihjat3.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihjat3.x ⊢ φ → X ∈ B
dihjat3.p ⊢ φ → P ∈ A
Assertion dihjat3 ⊢ φ → I ⁡ X ∨ ˙ P = I ⁡ X ⊕ ˙ I ⁡ P

Proof

Step Hyp Ref Expression
1 dihjat3.b ⊢ B = Base K
2 dihjat3.h ⊢ H = LHyp ⁡ K
3 dihjat3.j ⊢ ∨ ˙ = join ⁡ K
4 dihjat3.a ⊢ A = Atoms ⁡ K
5 dihjat3.u ⊢ U = DVecH ⁡ K ⁡ W
6 dihjat3.s ⊢ ⊕ ˙ = LSSum ⁡ U
7 dihjat3.i ⊢ I = DIsoH ⁡ K ⁡ W
8 dihjat3.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dihjat3.x ⊢ φ → X ∈ B
10 dihjat3.p ⊢ φ → P ∈ A
11 1 4 atbase ⊢ P ∈ A → P ∈ B
12 10 11 syl ⊢ φ → P ∈ B
13 eqid ⊢ joinH ⁡ K ⁡ W = joinH ⁡ K ⁡ W
14 1 3 2 7 13 djhlj ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ B → I ⁡ X ∨ ˙ P = I ⁡ X joinH ⁡ K ⁡ W I ⁡ P
15 8 9 12 14 syl12anc ⊢ φ → I ⁡ X ∨ ˙ P = I ⁡ X joinH ⁡ K ⁡ W I ⁡ P
16 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
17 1 2 7 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ∈ ran ⁡ I
18 8 9 17 syl2anc ⊢ φ → I ⁡ X ∈ ran ⁡ I
19 4 2 5 7 16 dihatlat ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A → I ⁡ P ∈ LSAtoms ⁡ U
20 8 10 19 syl2anc ⊢ φ → I ⁡ P ∈ LSAtoms ⁡ U
21 2 7 13 5 6 16 8 18 20 dihjat2 ⊢ φ → I ⁡ X joinH ⁡ K ⁡ W I ⁡ P = I ⁡ X ⊕ ˙ I ⁡ P
22 15 21 eqtrd ⊢ φ → I ⁡ X ∨ ˙ P = I ⁡ X ⊕ ˙ I ⁡ P