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

Metamath Proof Explorer

Theorem latj12

Description: Swap 1st and 2nd members of lattice join. ( chj12 analog.) (Contributed by NM, 4-Jun-2012)

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

Proof

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