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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ 𝑍 ) = ( ( 𝑋 ∨ 𝑍 ) ∨ 𝑌 ) )