This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latj32

Description: Swap 2nd and 3rd members of lattice join. Lemma 2.2 in MegPav2002 p. 362. (Contributed by NM, 2-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ B = Base K
2 latjass.j ⊢ ∨ ˙ = join ⁡ K
3 1 2 latjcom ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z = Z ∨ ˙ Y
4 3 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z = Z ∨ ˙ Y
5 4 oveq2d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Z ∨ ˙ Y
6 1 2 latjass ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Y ∨ ˙ Z
7 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
8 simpr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
9 simpr2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
10 7 8 9 3jca ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B ∧ Z ∈ B ∧ Y ∈ B
11 1 2 latjass ⊢ K ∈ Lat ∧ X ∈ B ∧ Z ∈ B ∧ Y ∈ B → X ∨ ˙ Z ∨ ˙ Y = X ∨ ˙ Z ∨ ˙ Y
12 10 11 syldan ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Z ∨ ˙ Y = X ∨ ˙ Z ∨ ˙ Y
13 5 6 12 3eqtr4d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∨ ˙ Y ∨ ˙ Z = X ∨ ˙ Z ∨ ˙ Y