Step | Hyp | Ref
| Expression |
1 | | cvrat2.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΎ) |
2 | | cvrat2.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
3 | | eqid 2733 |
. . . . . . . . 9
β’
(0.βπΎ) =
(0.βπΎ) |
4 | | cvrat2.c |
. . . . . . . . 9
β’ πΆ = ( β βπΎ) |
5 | | cvrat2.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
6 | 1, 2, 3, 4, 5 | atcvrj0 37937 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π)) β (π = (0.βπΎ) β π = π)) |
7 | 6 | 3expa 1119 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ππΆ(π β¨ π)) β (π = (0.βπΎ) β π = π)) |
8 | 7 | necon3bid 2985 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ππΆ(π β¨ π)) β (π β (0.βπΎ) β π β π)) |
9 | | simpl 484 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
10 | | simpr1 1195 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
11 | | hllat 37871 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β Lat) |
12 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
13 | | simpr2 1196 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
14 | 1, 5 | atbase 37797 |
. . . . . . . . . . 11
β’ (π β π΄ β π β π΅) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
16 | | simpr3 1197 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
17 | 1, 5 | atbase 37797 |
. . . . . . . . . . 11
β’ (π β π΄ β π β π΅) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
19 | 1, 2 | latjcl 18333 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
20 | 12, 15, 18, 19 | syl3anc 1372 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β π΅) |
21 | | eqid 2733 |
. . . . . . . . . . 11
β’
(ltβπΎ) =
(ltβπΎ) |
22 | 1, 21, 4 | cvrlt 37778 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ (π β¨ π) β π΅) β§ ππΆ(π β¨ π)) β π(ltβπΎ)(π β¨ π)) |
23 | 22 | ex 414 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΅ β§ (π β¨ π) β π΅) β (ππΆ(π β¨ π) β π(ltβπΎ)(π β¨ π))) |
24 | 9, 10, 20, 23 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (ππΆ(π β¨ π) β π(ltβπΎ)(π β¨ π))) |
25 | 1, 21, 2, 3, 5 | cvrat 37931 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β (0.βπΎ) β§ π(ltβπΎ)(π β¨ π)) β π β π΄)) |
26 | 25 | expcomd 418 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(ltβπΎ)(π β¨ π) β (π β (0.βπΎ) β π β π΄))) |
27 | 24, 26 | syld 47 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (ππΆ(π β¨ π) β (π β (0.βπΎ) β π β π΄))) |
28 | 27 | imp 408 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ππΆ(π β¨ π)) β (π β (0.βπΎ) β π β π΄)) |
29 | 8, 28 | sylbird 260 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ππΆ(π β¨ π)) β (π β π β π β π΄)) |
30 | 29 | ex 414 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (ππΆ(π β¨ π) β (π β π β π β π΄))) |
31 | 30 | com23 86 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β π β (ππΆ(π β¨ π) β π β π΄))) |
32 | 31 | impd 412 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ ππΆ(π β¨ π)) β π β π΄)) |
33 | 32 | 3impia 1118 |
1
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ ππΆ(π β¨ π))) β π β π΄) |