Metamath Proof Explorer

Theorem latjjdir

Description: Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012)

Ref Expression
Hypotheses latjass.b ⊢ B = Base K
latjass.j ⊢ ∨ ˙ = join ⁡ K
Assertion latjjdir ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Z ∨ ˙ Y ∨ ˙ Z

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ B = Base K
2 latjass.j ⊢ ∨ ˙ = join ⁡ K
3 1 2 latjidm ⊢ K ∈ Lat ∧ Z ∈ B → Z ∨ ˙ Z = Z
4 3 3ad2antr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∨ ˙ Z = Z
5 4 oveq2d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z ∨ ˙ Z = X ∨ ˙ Y ∨ ˙ Z
6 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
7 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
8 simpr2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
9 simpr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
10 1 2 latj4 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z ∨ ˙ Z = X ∨ ˙ Z ∨ ˙ Y ∨ ˙ Z
11 6 7 8 9 9 10 syl122anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z ∨ ˙ Z = X ∨ ˙ Z ∨ ˙ Y ∨ ˙ Z
12 5 11 eqtr3d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Z ∨ ˙ Y ∨ ˙ Z