This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∨ ( 𝑦 ∧ 𝑧 ) ) = ( ( 𝑥 ∨ 𝑦 ) ∧ ( 𝑥 ∨ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ) )