Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β πΉ = ( I βΎ π΅)) |
2 | 1 | fveq1d 6845 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β (πΉβπ) = (( I βΎ π΅)βπ)) |
3 | | simpl3l 1229 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β π β π΄) |
4 | | ltrnnidn.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
5 | | ltrnnidn.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β π΅) |
7 | | fvresi 7120 |
. . . . 5
β’ (π β π΅ β (( I βΎ π΅)βπ) = π) |
8 | 3, 6, 7 | 3syl 18 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β (( I βΎ π΅)βπ) = π) |
9 | 2, 8 | eqtrd 2777 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = ( I βΎ π΅)) β (πΉβπ) = π) |
10 | 9 | ex 414 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |
11 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β (πΎ β HL β§ π β π»)) |
12 | | simpl2 1193 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β πΉ β π) |
13 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β πΉ β ( I βΎ π΅)) |
14 | | simpl3 1194 |
. . . . 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 38640 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π) |
19 | 11, 12, 13, 14, 18 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β ( I βΎ π΅)) β (πΉβπ) β π) |
20 | 19 | ex 414 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ β ( I βΎ π΅) β (πΉβπ) β π)) |
21 | 20 | necon4d 2968 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) = π β πΉ = ( I βΎ π΅))) |
22 | 10, 21 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) |