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