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