Step | Hyp | Ref
| Expression |
1 | | trlnidatb.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | trlnidatb.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
3 | | trlnidatb.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | | trlnidatb.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
5 | | trlnidatb.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | trlnidat 39044 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (π
βπΉ) β π΄) |
7 | 6 | 3expia 1122 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ β ( I βΎ π΅) β (π
βπΉ) β π΄)) |
8 | | eqid 2733 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
9 | 8, 2, 3 | lhpexnle 38877 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β βπ β π΄ Β¬ π(leβπΎ)π) |
10 | 9 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β βπ β π΄ Β¬ π(leβπΎ)π) |
11 | 1, 8, 2, 3, 4 | ltrnideq 39046 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |
12 | 11 | 3expa 1119 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |
13 | | simp1l 1198 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π) β§ (πΉβπ) = π) β (πΎ β HL β§ π β π»)) |
14 | | simp2 1138 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π) β§ (πΉβπ) = π) β (π β π΄ β§ Β¬ π(leβπΎ)π)) |
15 | | simp1r 1199 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π) β§ (πΉβπ) = π) β πΉ β π) |
16 | | simp3 1139 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π) β§ (πΉβπ) = π) β (πΉβπ) = π) |
17 | | eqid 2733 |
. . . . . . . . 9
β’
(0.βπΎ) =
(0.βπΎ) |
18 | 8, 17, 2, 3, 4, 5 | trl0 39041 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π(leβπΎ)π) β§ (πΉ β π β§ (πΉβπ) = π)) β (π
βπΉ) = (0.βπΎ)) |
19 | 13, 14, 15, 16, 18 | syl112anc 1375 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π) β§ (πΉβπ) = π) β (π
βπΉ) = (0.βπΎ)) |
20 | 19 | 3expia 1122 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β ((πΉβπ) = π β (π
βπΉ) = (0.βπΎ))) |
21 | | simplll 774 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β πΎ β HL) |
22 | | hlatl 38230 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β AtLat) |
23 | 17, 2 | atn0 38178 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ (π
βπΉ) β π΄) β (π
βπΉ) β (0.βπΎ)) |
24 | 23 | ex 414 |
. . . . . . . 8
β’ (πΎ β AtLat β ((π
βπΉ) β π΄ β (π
βπΉ) β (0.βπΎ))) |
25 | 21, 22, 24 | 3syl 18 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β ((π
βπΉ) β π΄ β (π
βπΉ) β (0.βπΎ))) |
26 | 25 | necon2bd 2957 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β ((π
βπΉ) = (0.βπΎ) β Β¬ (π
βπΉ) β π΄)) |
27 | 20, 26 | syld 47 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β ((πΉβπ) = π β Β¬ (π
βπΉ) β π΄)) |
28 | 12, 27 | sylbid 239 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (πΉ = ( I βΎ π΅) β Β¬ (π
βπΉ) β π΄)) |
29 | 10, 28 | rexlimddv 3162 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ = ( I βΎ π΅) β Β¬ (π
βπΉ) β π΄)) |
30 | 29 | necon2ad 2956 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π
βπΉ) β π΄ β πΉ β ( I βΎ π΅))) |
31 | 7, 30 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ β ( I βΎ π΅) β (π
βπΉ) β π΄)) |