Step | Hyp | Ref
| Expression |
1 | | simpr 484 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β πΉ = ( I βΎ π΅)) |
2 | 1 | fveq1d 6887 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β (πΉβπ) = (( I βΎ π΅)βπ)) |
3 | | simpl3l 1225 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β π β π΄) |
4 | | ltrnnidn.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
5 | | ltrnnidn.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | atbase 38672 |
. . . . 5
β’ (π β π΄ β π β π΅) |
7 | | fvresi 7167 |
. . . . 5
β’ (π β π΅ β (( I βΎ π΅)βπ) = π) |
8 | 3, 6, 7 | 3syl 18 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β (( I βΎ π΅)βπ) = π) |
9 | 2, 8 | eqtrd 2766 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β (πΉβπ) = π) |
10 | 9 | ex 412 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |
11 | | simpl1 1188 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β (πΎ β HL β§ π β π»)) |
12 | | simpl2 1189 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β πΉ β π) |
13 | | simpr 484 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β πΉ β ( I βΎ π΅)) |
14 | | simpl3 1190 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β (π β π΄ β§ Β¬ π β€ π)) |
15 | | ltrnnidn.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
16 | | ltrnnidn.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
17 | | ltrnnidn.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
18 | 4, 15, 5, 16, 17 | ltrnnidn 39558 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π) |
19 | 11, 12, 13, 14, 18 | syl121anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β (πΉβπ) β π) |
20 | 19 | ex 412 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ β ( I βΎ π΅) β (πΉβπ) β π)) |
21 | 20 | necon4d 2958 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) = π β πΉ = ( I βΎ π΅))) |
22 | 10, 21 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |