Step |
Hyp |
Ref |
Expression |
1 |
|
dalem.ph |
⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) ) |
2 |
|
dalem.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
dalem.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
4 |
|
dalem.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
dalem.ps |
⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) |
6 |
|
dalem21.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
7 |
|
dalem21.o |
⊢ 𝑂 = ( LPlanes ‘ 𝐾 ) |
8 |
|
dalem21.y |
⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) |
9 |
|
dalem21.z |
⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 ) |
10 |
1
|
dalemkehl |
⊢ ( 𝜑 → 𝐾 ∈ HL ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → 𝐾 ∈ HL ) |
12 |
1 2 3 4 5
|
dalemcjden |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) ) |
13 |
12
|
3adant2 |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) ) |
14 |
1 2 3 4 7 8
|
dalempjsen |
⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) |
16 |
1 2 3 4 7 8
|
dalemply |
⊢ ( 𝜑 → 𝑃 ≤ 𝑌 ) |
17 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑃 ≤ 𝑌 ) |
18 |
1 2 3 4 9
|
dalemsly |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑆 ≤ 𝑌 ) |
19 |
1
|
dalemkelat |
⊢ ( 𝜑 → 𝐾 ∈ Lat ) |
20 |
1 4
|
dalempeb |
⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
21 |
1 4
|
dalemseb |
⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ 𝐾 ) ) |
22 |
1 7
|
dalemyeb |
⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
23 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
24 |
23 2 3
|
latjle12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑌 ∧ 𝑆 ≤ 𝑌 ) ↔ ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) ) |
25 |
19 20 21 22 24
|
syl13anc |
⊢ ( 𝜑 → ( ( 𝑃 ≤ 𝑌 ∧ 𝑆 ≤ 𝑌 ) ↔ ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) ) |
26 |
25
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( ( 𝑃 ≤ 𝑌 ∧ 𝑆 ≤ 𝑌 ) ↔ ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) ) |
27 |
17 18 26
|
mpbi2and |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) |
28 |
27
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ) |
29 |
5
|
dalem-ccly |
⊢ ( 𝜓 → ¬ 𝑐 ≤ 𝑌 ) |
30 |
29
|
adantl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ 𝑐 ≤ 𝑌 ) |
31 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 ∈ Lat ) |
32 |
5 4
|
dalemcceb |
⊢ ( 𝜓 → 𝑐 ∈ ( Base ‘ 𝐾 ) ) |
33 |
32
|
adantl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑐 ∈ ( Base ‘ 𝐾 ) ) |
34 |
5
|
dalemddea |
⊢ ( 𝜓 → 𝑑 ∈ 𝐴 ) |
35 |
23 4
|
atbase |
⊢ ( 𝑑 ∈ 𝐴 → 𝑑 ∈ ( Base ‘ 𝐾 ) ) |
36 |
34 35
|
syl |
⊢ ( 𝜓 → 𝑑 ∈ ( Base ‘ 𝐾 ) ) |
37 |
36
|
adantl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑑 ∈ ( Base ‘ 𝐾 ) ) |
38 |
23 2 3
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ 𝑑 ∈ ( Base ‘ 𝐾 ) ) → 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) ) |
39 |
31 33 37 38
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) ) |
40 |
|
eqid |
⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 ) |
41 |
23 40
|
llnbase |
⊢ ( ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ) |
42 |
12 41
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ) |
43 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
44 |
23 2
|
lattr |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑐 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) → 𝑐 ≤ 𝑌 ) ) |
45 |
31 33 42 43 44
|
syl13anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ≤ ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) → 𝑐 ≤ 𝑌 ) ) |
46 |
39 45
|
mpand |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 → 𝑐 ≤ 𝑌 ) ) |
47 |
30 46
|
mtod |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ¬ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) |
48 |
47
|
3adant2 |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ¬ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) |
49 |
|
nbrne2 |
⊢ ( ( ( 𝑃 ∨ 𝑆 ) ≤ 𝑌 ∧ ¬ ( 𝑐 ∨ 𝑑 ) ≤ 𝑌 ) → ( 𝑃 ∨ 𝑆 ) ≠ ( 𝑐 ∨ 𝑑 ) ) |
50 |
28 48 49
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ≠ ( 𝑐 ∨ 𝑑 ) ) |
51 |
50
|
necomd |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( 𝑐 ∨ 𝑑 ) ≠ ( 𝑃 ∨ 𝑆 ) ) |
52 |
|
hlatl |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat ) |
53 |
10 52
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ AtLat ) |
54 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 ∈ AtLat ) |
55 |
1
|
dalempea |
⊢ ( 𝜑 → 𝑃 ∈ 𝐴 ) |
56 |
1
|
dalemsea |
⊢ ( 𝜑 → 𝑆 ∈ 𝐴 ) |
57 |
23 3 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
58 |
10 55 56 57
|
syl3anc |
⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
59 |
58
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) |
60 |
23 6
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
61 |
31 42 59 60
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) |
62 |
1 2 3 4 7 8
|
dalemcea |
⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) |
63 |
62
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ 𝐴 ) |
64 |
5
|
dalemclccjdd |
⊢ ( 𝜓 → 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) |
65 |
64
|
adantl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) |
66 |
1
|
dalemclpjs |
⊢ ( 𝜑 → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) |
67 |
66
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) |
68 |
1 4
|
dalemceb |
⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐾 ) ) |
69 |
68
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ ( Base ‘ 𝐾 ) ) |
70 |
23 2 6
|
latlem12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ↔ 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) ) |
71 |
31 69 42 59 70
|
syl13anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ↔ 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) ) |
72 |
65 67 71
|
mpbi2and |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) |
73 |
|
eqid |
⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 ) |
74 |
23 2 73 4
|
atlen0 |
⊢ ( ( ( 𝐾 ∈ AtLat ∧ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ 𝐴 ) ∧ 𝐶 ≤ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) ) |
75 |
54 61 63 72 74
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) ) |
76 |
75
|
3adant2 |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) ) |
77 |
6 73 4 40
|
2llnmat |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑐 ∨ 𝑑 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) ∧ ( ( 𝑐 ∨ 𝑑 ) ≠ ( 𝑃 ∨ 𝑆 ) ∧ ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≠ ( 0. ‘ 𝐾 ) ) ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ 𝐴 ) |
78 |
11 13 15 51 76 77
|
syl32anc |
⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓 ) → ( ( 𝑐 ∨ 𝑑 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ∈ 𝐴 ) |