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

Metamath Proof Explorer

Theorem latdisdlem

Description: Lemma for latdisd . (Contributed by Stefan O'Rear, 30-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 latdisd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latdisd.j ⊢ ∨ = ( join ‘ 𝐾 )
3 latdisd.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∧ 𝑦 ) ∈ 𝐵 )
5 4 3adant3r3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∧ 𝑦 ) ∈ 𝐵 )
6 simpr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
7 simpr3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
8 oveq1 ⊢ ( 𝑢 = ( 𝑥 ∧ 𝑦 ) → ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑣 ∧ 𝑤 ) ) )
9 oveq1 ⊢ ( 𝑢 = ( 𝑥 ∧ 𝑦 ) → ( 𝑢 ∨ 𝑣 ) = ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑣 ) )
10 oveq1 ⊢ ( 𝑢 = ( 𝑥 ∧ 𝑦 ) → ( 𝑢 ∨ 𝑤 ) = ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) )
11 9 10 oveq12d ⊢ ( 𝑢 = ( 𝑥 ∧ 𝑦 ) → ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑣 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) )
12 8 11 eqeq12d ⊢ ( 𝑢 = ( 𝑥 ∧ 𝑦 ) → ( ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ↔ ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑣 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) ) )
13 oveq1 ⊢ ( 𝑣 = 𝑥 → ( 𝑣 ∧ 𝑤 ) = ( 𝑥 ∧ 𝑤 ) )
14 13 oveq2d ⊢ ( 𝑣 = 𝑥 → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) )
15 oveq2 ⊢ ( 𝑣 = 𝑥 → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑣 ) = ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) )
16 15 oveq1d ⊢ ( 𝑣 = 𝑥 → ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑣 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑣 = 𝑥 → ( ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑣 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) ↔ ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) ) )
18 oveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∧ 𝑤 ) = ( 𝑥 ∧ 𝑧 ) )
19 18 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
20 oveq2 ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) = ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) )
21 20 oveq2d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) )
22 19 21 eqeq12d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑤 ) ) ↔ ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) ) )
23 12 17 22 rspc3v ⊢ ( ( ( 𝑥 ∧ 𝑦 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) ) )
24 5 6 7 23 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) ) )
25 24 imp ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) = ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) )
26 simpl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
27 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∧ 𝑦 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) = ( 𝑥 ∨ ( 𝑥 ∧ 𝑦 ) ) )
28 26 5 6 27 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) = ( 𝑥 ∨ ( 𝑥 ∧ 𝑦 ) ) )
29 1 2 3 latabs1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∨ ( 𝑥 ∧ 𝑦 ) ) = 𝑥 )
30 29 3adant3r3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∨ ( 𝑥 ∧ 𝑦 ) ) = 𝑥 )
31 28 30 eqtrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) = 𝑥 )
32 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∧ 𝑦 ) ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) = ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) )
33 26 5 7 32 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) = ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) )
34 31 33 oveq12d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) = ( 𝑥 ∧ ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) ) )
35 34 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑥 ) ∧ ( ( 𝑥 ∧ 𝑦 ) ∨ 𝑧 ) ) = ( 𝑥 ∧ ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) ) )
36 simpr2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
37 oveq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( 𝑧 ∨ ( 𝑣 ∧ 𝑤 ) ) )
38 oveq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∨ 𝑣 ) = ( 𝑧 ∨ 𝑣 ) )
39 oveq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∨ 𝑤 ) = ( 𝑧 ∨ 𝑤 ) )
40 38 39 oveq12d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑣 ) ∧ ( 𝑧 ∨ 𝑤 ) ) )
41 37 40 eqeq12d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ↔ ( 𝑧 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑣 ) ∧ ( 𝑧 ∨ 𝑤 ) ) ) )
42 13 oveq2d ⊢ ( 𝑣 = 𝑥 → ( 𝑧 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( 𝑧 ∨ ( 𝑥 ∧ 𝑤 ) ) )
43 oveq2 ⊢ ( 𝑣 = 𝑥 → ( 𝑧 ∨ 𝑣 ) = ( 𝑧 ∨ 𝑥 ) )
44 43 oveq1d ⊢ ( 𝑣 = 𝑥 → ( ( 𝑧 ∨ 𝑣 ) ∧ ( 𝑧 ∨ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑤 ) ) )
45 42 44 eqeq12d ⊢ ( 𝑣 = 𝑥 → ( ( 𝑧 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑣 ) ∧ ( 𝑧 ∨ 𝑤 ) ) ↔ ( 𝑧 ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑤 ) ) ) )
46 oveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∧ 𝑤 ) = ( 𝑥 ∧ 𝑦 ) )
47 46 oveq2d ⊢ ( 𝑤 = 𝑦 → ( 𝑧 ∨ ( 𝑥 ∧ 𝑤 ) ) = ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) )
48 oveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑧 ∨ 𝑤 ) = ( 𝑧 ∨ 𝑦 ) )
49 48 oveq2d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) )
50 47 49 eqeq12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑧 ∨ ( 𝑥 ∧ 𝑤 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑤 ) ) ↔ ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) )
51 41 45 50 rspc3v ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) → ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) )
52 7 6 36 51 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) → ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) )
53 52 imp ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) = ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) )
54 53 oveq2d ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( 𝑥 ∧ ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) ) = ( 𝑥 ∧ ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) )
55 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 ∨ 𝑥 ) ∈ 𝐵 )
56 26 7 6 55 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∨ 𝑥 ) ∈ 𝐵 )
57 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∨ 𝑦 ) ∈ 𝐵 )
58 26 7 36 57 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∨ 𝑦 ) ∈ 𝐵 )
59 1 3 latmass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∨ 𝑥 ) ∈ 𝐵 ∧ ( 𝑧 ∨ 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝑥 ∧ ( 𝑧 ∨ 𝑥 ) ) ∧ ( 𝑧 ∨ 𝑦 ) ) = ( 𝑥 ∧ ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) )
60 26 6 56 58 59 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∧ ( 𝑧 ∨ 𝑥 ) ) ∧ ( 𝑧 ∨ 𝑦 ) ) = ( 𝑥 ∧ ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) )
61 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 ∨ 𝑥 ) = ( 𝑥 ∨ 𝑧 ) )
62 26 7 6 61 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∨ 𝑥 ) = ( 𝑥 ∨ 𝑧 ) )
63 62 oveq2d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∧ ( 𝑧 ∨ 𝑥 ) ) = ( 𝑥 ∧ ( 𝑥 ∨ 𝑧 ) ) )
64 1 2 3 latabs2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ∧ ( 𝑥 ∨ 𝑧 ) ) = 𝑥 )
65 26 6 7 64 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∧ ( 𝑥 ∨ 𝑧 ) ) = 𝑥 )
66 63 65 eqtrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∧ ( 𝑧 ∨ 𝑥 ) ) = 𝑥 )
67 1 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∨ 𝑦 ) = ( 𝑦 ∨ 𝑧 ) )
68 26 7 36 67 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑧 ∨ 𝑦 ) = ( 𝑦 ∨ 𝑧 ) )
69 66 68 oveq12d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ∧ ( 𝑧 ∨ 𝑥 ) ) ∧ ( 𝑧 ∨ 𝑦 ) ) = ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) )
70 60 69 eqtr3d ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∧ ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) = ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) )
71 70 adantr ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( 𝑥 ∧ ( ( 𝑧 ∨ 𝑥 ) ∧ ( 𝑧 ∨ 𝑦 ) ) ) = ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) )
72 54 71 eqtrd ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( 𝑥 ∧ ( 𝑧 ∨ ( 𝑥 ∧ 𝑦 ) ) ) = ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) )
73 25 35 72 3eqtrrd ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
74 73 an32s ⊢ ( ( ( 𝐾 ∈ Lat ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
75 74 ralrimivvva ⊢ ( ( 𝐾 ∈ Lat ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) )
76 75 ex ⊢ ( 𝐾 ∈ Lat → ( ∀ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑢 ∨ ( 𝑣 ∧ 𝑤 ) ) = ( ( 𝑢 ∨ 𝑣 ) ∧ ( 𝑢 ∨ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ∧ ( 𝑦 ∨ 𝑧 ) ) = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ 𝑧 ) ) ) )