Metamath Proof Explorer

Theorem latjjdi

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

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

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ B = Base K
2 latjass.j ⊢ ∨ ˙ = join ⁡ K
3 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
4 1 2 latjidm ⊢ K ∈ Lat ∧ X ∈ B → X ∨ ˙ X = X
5 3 4 syldan ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ X = X
6 5 oveq1d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Y ∨ ˙ Z
7 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
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 ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Y ∨ ˙ X ∨ ˙ Z
11 7 3 3 8 9 10 syl122anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Y ∨ ˙ X ∨ ˙ Z
12 6 11 eqtr3d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Y ∨ ˙ X ∨ ˙ Z