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