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