Theorem latjcom

Description: The join of a lattice commutes. ( chjcom analog.) (Contributed by NM, 16-Sep-2011)

	Ref	Expression
Hypotheses	latjcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latjcom.j	⊢ ∨ = ( join ‘ 𝐾 )
Assertion	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		latjcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latjcom.j	⊢ ∨ = ( join ‘ 𝐾 )
3		opelxpi	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
4	3	3adant1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
5		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
6	1 2 5	islat	⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ( meet ‘ 𝐾 ) = ( 𝐵 × 𝐵 ) ) ) )
7		simprl	⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ( meet ‘ 𝐾 ) = ( 𝐵 × 𝐵 ) ) ) → 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	joincom	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∨ ) ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )
18	16 17	syl3anl1	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∨ ) ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )
19	15 18	mpdan	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )