Theorem latdisd

Description: In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	latdisd.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latdisd.j	⊢ ∨ = ( join ‘ 𝐾 )
	latdisd.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latdisd	⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		latdisd.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latdisd.j	⊢ ∨ = ( join ‘ 𝐾 )
3		latdisd.m	⊢ ∧ = ( meet ‘ 𝐾 )
4	1 2 3	latdisdlem	⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) ) )
5		eqid	⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
6	5	odulat	⊢ ( 𝐾 ∈ Lat → ( ODual ‘ 𝐾 ) ∈ Lat )
7	5 1	odubas	⊢ 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) )
8	5 3	odujoin	⊢ ∧ = ( join ‘ ( ODual ‘ 𝐾 ) )
9	5 2	odumeet	⊢ ∨ = ( meet ‘ ( ODual ‘ 𝐾 ) )
10	7 8 9	latdisdlem	⊢ ( ( ODual ‘ 𝐾 ) ∈ Lat → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) ) )
11	6 10	syl	⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) ) )
12	4 11	impbid	⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) ) )
13		oveq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( 𝑥 ∧ ( 𝑣 ∨ 𝑤 ) ) )
14		oveq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∧ 𝑣 ) = ( 𝑥 ∧ 𝑣 ) )
15		oveq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∧ 𝑤 ) = ( 𝑥 ∧ 𝑤 ) )
16	14 15	oveq12d	⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑣 ) ∨ ( 𝑥 ∧ 𝑤 ) ) )
17	13 16	eqeq12d	⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) ↔ ( 𝑥 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑣 ) ∨ ( 𝑥 ∧ 𝑤 ) ) ) )
18		oveq1	⊢ ( 𝑣 = 𝑦 → ( 𝑣 ∨ 𝑤 ) = ( 𝑦 ∨ 𝑤 ) )
19	18	oveq2d	⊢ ( 𝑣 = 𝑦 → ( 𝑥 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( 𝑥 ∧ ( 𝑦 ∨ 𝑤 ) ) )
20		oveq2	⊢ ( 𝑣 = 𝑦 → ( 𝑥 ∧ 𝑣 ) = ( 𝑥 ∧ 𝑦 ) )
21	20	oveq1d	⊢ ( 𝑣 = 𝑦 → ( ( 𝑥 ∧ 𝑣 ) ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) )
22	19 21	eqeq12d	⊢ ( 𝑣 = 𝑦 → ( ( 𝑥 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑣 ) ∨ ( 𝑥 ∧ 𝑤 ) ) ↔ ( 𝑥 ∧ ( 𝑦 ∨ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) ) )
23		oveq2	⊢ ( 𝑤 = 𝑧 → ( 𝑦 ∨ 𝑤 ) = ( 𝑦 ∨ 𝑧 ) )
24	23	oveq2d	⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∧ ( 𝑦 ∨ 𝑤 ) ) = ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) )
25		oveq2	⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∧ 𝑤 ) = ( 𝑥 ∧ 𝑧 ) )
26	25	oveq2d	⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
27	24 26	eqeq12d	⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∧ ( 𝑦 ∨ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) ↔ ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ) )
28	17 22 27	cbvral3vw	⊢ ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∧ ( 𝑣 ∨ 𝑤 ) ) = ( ( 𝑢 ∧ 𝑣 ) ∨ ( 𝑢 ∧ 𝑤 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
29	12 28	bitrdi	⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ) )