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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
latjass.j ⊢ ∨ = ( join ‘ 𝐾 )
Assertion latj32 ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) = ( ( 𝑋 ∨ 𝑍 ) ∨ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 latjass.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latjass.j ⊢ ∨ = ( join ‘ 𝐾 )
3 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑍 ) = ( 𝑍 ∨ 𝑌 ) )
4 3 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑍 ) = ( 𝑍 ∨ 𝑌 ) )
5 4 oveq2d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) = ( 𝑋 ∨ ( 𝑍 ∨ 𝑌 ) ) )
6 1 2 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) = ( 𝑋 ∨ ( 𝑌 ∨ 𝑍 ) ) )
7 simpr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
8 simpr3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
9 simpr2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
10 7 8 9 3jca ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
11 1 2 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑍 ) ∨ 𝑌 ) = ( 𝑋 ∨ ( 𝑍 ∨ 𝑌 ) ) )
12 10 11 syldan ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑍 ) ∨ 𝑌 ) = ( 𝑋 ∨ ( 𝑍 ∨ 𝑌 ) ) )
13 5 6 12 3eqtr4d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) = ( ( 𝑋 ∨ 𝑍 ) ∨ 𝑌 ) )