Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β HL) |
2 | | hlatl 37825 |
. . . 4
β’ (πΎ β HL β πΎ β AtLat) |
3 | 1, 2 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β AtLat) |
4 | | simp1 1137 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
5 | | simp2l 1200 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
6 | | simp2r 1201 |
. . . 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 2737 |
. . . . 5
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
12 | 7, 8, 9, 10, 11 | trlnidat 38639 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (((trLβπΎ)βπ)βπΉ) β π΄) |
13 | 4, 5, 6, 12 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (((trLβπΎ)βπ)βπΉ) β π΄) |
14 | | eqid 2737 |
. . . 4
β’
(0.βπΎ) =
(0.βπΎ) |
15 | 14, 8 | atn0 37773 |
. . 3
β’ ((πΎ β AtLat β§
(((trLβπΎ)βπ)βπΉ) β π΄) β (((trLβπΎ)βπ)βπΉ) β (0.βπΎ)) |
16 | 3, 13, 15 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (((trLβπΎ)βπ)βπΉ) β (0.βπΎ)) |
17 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΎ β HL β§ π β π»)) |
18 | | simpl3 1194 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (π β π΄ β§ Β¬ π β€ π)) |
19 | | simpl2l 1227 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β πΉ β π) |
20 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = π) |
21 | | ltrnnidn.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
22 | 21, 14, 8, 9, 10, 11 | trl0 38636 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) = π)) β (((trLβπΎ)βπ)βπΉ) = (0.βπΎ)) |
23 | 17, 18, 19, 20, 22 | syl112anc 1375 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (((trLβπΎ)βπ)βπΉ) = (0.βπΎ)) |
24 | 23 | ex 414 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) = π β (((trLβπΎ)βπ)βπΉ) = (0.βπΎ))) |
25 | 24 | necon3d 2965 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((((trLβπΎ)βπ)βπΉ) β (0.βπΎ) β (πΉβπ) β π)) |
26 | 16, 25 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π) |