Step | Hyp | Ref
| Expression |
1 | | simp1l 1197 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β HL) |
2 | | hlatl 38218 |
. . . 4
β’ (πΎ β HL β πΎ β AtLat) |
3 | 1, 2 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β AtLat) |
4 | | simp1 1136 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
5 | | simp2l 1199 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
6 | | simp2r 1200 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β ( I βΎ π΅)) |
7 | | ltrnnidn.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
8 | | ltrnnidn.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
9 | | ltrnnidn.h |
. . . . 5
β’ π» = (LHypβπΎ) |
10 | | ltrnnidn.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
11 | | eqid 2732 |
. . . . 5
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
12 | 7, 8, 9, 10, 11 | trlnidat 39032 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (((trLβπΎ)βπ)βπΉ) β π΄) |
13 | 4, 5, 6, 12 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (((trLβπΎ)βπ)βπΉ) β π΄) |
14 | | eqid 2732 |
. . . 4
β’
(0.βπΎ) =
(0.βπΎ) |
15 | 14, 8 | atn0 38166 |
. . 3
β’ ((πΎ β AtLat β§
(((trLβπΎ)βπ)βπΉ) β π΄) β (((trLβπΎ)βπ)βπΉ) β (0.βπΎ)) |
16 | 3, 13, 15 | syl2anc 584 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (((trLβπΎ)βπ)βπΉ) β (0.βπΎ)) |
17 | | simpl1 1191 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΎ β HL β§ π β π»)) |
18 | | simpl3 1193 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (π β π΄ β§ Β¬ π β€ π)) |
19 | | simpl2l 1226 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β πΉ β π) |
20 | | simpr 485 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = π) |
21 | | ltrnnidn.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
22 | 21, 14, 8, 9, 10, 11 | trl0 39029 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) = π)) β (((trLβπΎ)βπ)βπΉ) = (0.βπΎ)) |
23 | 17, 18, 19, 20, 22 | syl112anc 1374 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (((trLβπΎ)βπ)βπΉ) = (0.βπΎ)) |
24 | 23 | ex 413 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) = π β (((trLβπΎ)βπ)βπΉ) = (0.βπΎ))) |
25 | 24 | necon3d 2961 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((((trLβπΎ)βπ)βπΉ) β (0.βπΎ) β (πΉβπ) β π)) |
26 | 16, 25 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π) |