Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . . . 8
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β πΎ β HL) |
2 | | simpl2 1193 |
. . . . . . . 8
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β πΉ β πΌ) |
3 | | lauteq.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
4 | | lauteq.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | atbase 38207 |
. . . . . . . . 9
β’ (π β π΄ β π β π΅) |
6 | 5 | adantl 483 |
. . . . . . . 8
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β π β π΅) |
7 | | simpl3 1194 |
. . . . . . . 8
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β π β π΅) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(leβπΎ) =
(leβπΎ) |
9 | | lauteq.i |
. . . . . . . . 9
β’ πΌ = (LAutβπΎ) |
10 | 3, 8, 9 | lautle 39003 |
. . . . . . . 8
β’ (((πΎ β HL β§ πΉ β πΌ) β§ (π β π΅ β§ π β π΅)) β (π(leβπΎ)π β (πΉβπ)(leβπΎ)(πΉβπ))) |
11 | 1, 2, 6, 7, 10 | syl22anc 838 |
. . . . . . 7
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β (π(leβπΎ)π β (πΉβπ)(leβπΎ)(πΉβπ))) |
12 | | breq1 5152 |
. . . . . . 7
β’ ((πΉβπ) = π β ((πΉβπ)(leβπΎ)(πΉβπ) β π(leβπΎ)(πΉβπ))) |
13 | 11, 12 | sylan9bb 511 |
. . . . . 6
β’ ((((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β§ (πΉβπ) = π) β (π(leβπΎ)π β π(leβπΎ)(πΉβπ))) |
14 | 13 | bicomd 222 |
. . . . 5
β’ ((((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β§ (πΉβπ) = π) β (π(leβπΎ)(πΉβπ) β π(leβπΎ)π)) |
15 | 14 | ex 414 |
. . . 4
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ π β π΄) β ((πΉβπ) = π β (π(leβπΎ)(πΉβπ) β π(leβπΎ)π))) |
16 | 15 | ralimdva 3168 |
. . 3
β’ ((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β (βπ β π΄ (πΉβπ) = π β βπ β π΄ (π(leβπΎ)(πΉβπ) β π(leβπΎ)π))) |
17 | 16 | imp 408 |
. 2
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β βπ β π΄ (π(leβπΎ)(πΉβπ) β π(leβπΎ)π)) |
18 | | simpl1 1192 |
. . 3
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β πΎ β HL) |
19 | | simpl2 1193 |
. . . 4
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β πΉ β πΌ) |
20 | | simpl3 1194 |
. . . 4
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β π β π΅) |
21 | 3, 9 | lautcl 39006 |
. . . 4
β’ (((πΎ β HL β§ πΉ β πΌ) β§ π β π΅) β (πΉβπ) β π΅) |
22 | 18, 19, 20, 21 | syl21anc 837 |
. . 3
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β (πΉβπ) β π΅) |
23 | 3, 8, 4 | hlateq 38318 |
. . 3
β’ ((πΎ β HL β§ (πΉβπ) β π΅ β§ π β π΅) β (βπ β π΄ (π(leβπΎ)(πΉβπ) β π(leβπΎ)π) β (πΉβπ) = π)) |
24 | 18, 22, 20, 23 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β (βπ β π΄ (π(leβπΎ)(πΉβπ) β π(leβπΎ)π) β (πΉβπ) = π)) |
25 | 17, 24 | mpbid 231 |
1
β’ (((πΎ β HL β§ πΉ β πΌ β§ π β π΅) β§ βπ β π΄ (πΉβπ) = π) β (πΉβπ) = π) |