Theorem latmcom

Description: The join of a lattice commutes. (Contributed by NM, 6-Nov-2011)

	Ref	Expression
Hypotheses	latmcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latmcom.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latmcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		latmcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latmcom.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		opelxpi	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
4	3	3adant1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
5		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6	1 5 2	islat	⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( join ‘ 𝐾 ) = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )
7		simprr	⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ( join ‘ 𝐾 ) = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) → dom ∧ = ( 𝐵 × 𝐵 ) )
8	6 7	sylbi	⊢ ( 𝐾 ∈ Lat → dom ∧ = ( 𝐵 × 𝐵 ) )
9	8	3ad2ant1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → dom ∧ = ( 𝐵 × 𝐵 ) )
10	4 9	eleqtrrd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
11		opelxpi	⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ⟨ 𝑌 , 𝑋 ⟩ ∈ ( 𝐵 × 𝐵 ) )
12	11	ancoms	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑌 , 𝑋 ⟩ ∈ ( 𝐵 × 𝐵 ) )
13	12	3adant1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑌 , 𝑋 ⟩ ∈ ( 𝐵 × 𝐵 ) )
14	13 9	eleqtrrd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∧ )
15	10 14	jca	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∧ ) )
16		latpos	⊢ ( 𝐾 ∈ Lat → 𝐾 ∈ Poset )
17	1 2	meetcom	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∧ ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
18	16 17	syl3anl1	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∧ ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
19	15 18	mpdan	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )