Theorem dlatjmdi

Description: In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	dlatjmdi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dlatjmdi.j	⊢ ∨ = ( join ‘ 𝐾 )
	dlatjmdi.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	dlatjmdi	⊢ ( ( 𝐾 ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dlatjmdi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dlatjmdi.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dlatjmdi.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		eqid	⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
5	4	odudlatb	⊢ ( 𝐾 ∈ DLat → ( 𝐾 ∈ DLat ↔ ( ODual ‘ 𝐾 ) ∈ DLat ) )
6	5	ibi	⊢ ( 𝐾 ∈ DLat → ( ODual ‘ 𝐾 ) ∈ DLat )
7	4 1	odubas	⊢ 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) )
8	4 3	odujoin	⊢ ∧ = ( join ‘ ( ODual ‘ 𝐾 ) )
9	4 2	odumeet	⊢ ∨ = ( meet ‘ ( ODual ‘ 𝐾 ) )
10	7 8 9	dlatmjdi	⊢ ( ( ( ODual ‘ 𝐾 ) ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )
11	6 10	sylan	⊢ ( ( 𝐾 ∈ DLat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑍 ) ) )