Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β (πΎ β HL β§ π β π»)) |
2 | | simpl2l 1227 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β π β πΈ) |
3 | | tendotr.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | tendotr.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
5 | | tendotr.e |
. . . . . 6
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | 3, 4, 5 | tendoid 39239 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
7 | 1, 2, 6 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
8 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β πΉ = ( I βΎ π΅)) |
9 | 8 | fveq2d 6847 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β (πβπΉ) = (πβ( I βΎ π΅))) |
10 | 7, 9, 8 | 3eqtr4d 2787 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β (πβπΉ) = πΉ) |
11 | 10 | fveq2d 6847 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ = ( I βΎ π΅)) β (π
β(πβπΉ)) = (π
βπΉ)) |
12 | | simpl1 1192 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (πΎ β HL β§ π β π»)) |
13 | | simpl2l 1227 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β π β πΈ) |
14 | | simpl3 1194 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β πΉ β π) |
15 | | eqid 2737 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
16 | | tendotr.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
17 | | tendotr.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
18 | 15, 4, 16, 17, 5 | tendotp 39227 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π
β(πβπΉ))(leβπΎ)(π
βπΉ)) |
19 | 12, 13, 14, 18 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (π
β(πβπΉ))(leβπΎ)(π
βπΉ)) |
20 | | simpl1l 1225 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β πΎ β HL) |
21 | | hlatl 37825 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
22 | 20, 21 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β πΎ β AtLat) |
23 | 4, 16, 5 | tendocl 39233 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
24 | 12, 13, 14, 23 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (πβπΉ) β π) |
25 | | simpl2r 1228 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β π β π) |
26 | | simpr 486 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β πΉ β ( I βΎ π΅)) |
27 | | tendotr.o |
. . . . . . . . 9
β’ π = (π β π β¦ ( I βΎ π΅)) |
28 | 3, 4, 16, 5, 27 | tendoid0 39291 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β ((πβπΉ) = ( I βΎ π΅) β π = π)) |
29 | 12, 13, 14, 26, 28 | syl112anc 1375 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β ((πβπΉ) = ( I βΎ π΅) β π = π)) |
30 | 29 | necon3bid 2989 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β ((πβπΉ) β ( I βΎ π΅) β π β π)) |
31 | 25, 30 | mpbird 257 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (πβπΉ) β ( I βΎ π΅)) |
32 | | eqid 2737 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
33 | 3, 32, 4, 16, 17 | trlnidat 38639 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π β§ (πβπΉ) β ( I βΎ π΅)) β (π
β(πβπΉ)) β (AtomsβπΎ)) |
34 | 12, 24, 31, 33 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (π
β(πβπΉ)) β (AtomsβπΎ)) |
35 | 3, 32, 4, 16, 17 | trlnidat 38639 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (π
βπΉ) β (AtomsβπΎ)) |
36 | 12, 14, 26, 35 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (π
βπΉ) β (AtomsβπΎ)) |
37 | 15, 32 | atcmp 37776 |
. . . 4
β’ ((πΎ β AtLat β§ (π
β(πβπΉ)) β (AtomsβπΎ) β§ (π
βπΉ) β (AtomsβπΎ)) β ((π
β(πβπΉ))(leβπΎ)(π
βπΉ) β (π
β(πβπΉ)) = (π
βπΉ))) |
38 | 22, 34, 36, 37 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β ((π
β(πβπΉ))(leβπΎ)(π
βπΉ) β (π
β(πβπΉ)) = (π
βπΉ))) |
39 | 19, 38 | mpbid 231 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β§ πΉ β ( I βΎ π΅)) β (π
β(πβπΉ)) = (π
βπΉ)) |
40 | 11, 39 | pm2.61dane 3033 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β (π
β(πβπΉ)) = (π
βπΉ)) |