Step | Hyp | Ref
| Expression |
1 | | erng1.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | erng1.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
3 | | erng1.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | 1, 2, 3 | tendoidcl 39282 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
5 | | erng1.d |
. . . 4
β’ π· = ((EDRingβπΎ)βπ) |
6 | | eqid 2733 |
. . . 4
β’
(Baseβπ·) =
(Baseβπ·) |
7 | 1, 2, 3, 5, 6 | erngbase 39314 |
. . 3
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
8 | 4, 7 | eleqtrrd 2837 |
. 2
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β (Baseβπ·)) |
9 | 7 | eleq2d 2820 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (π’ β (Baseβπ·) β π’ β πΈ)) |
10 | | simpl 484 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (πΎ β HL β§ π β π»)) |
11 | 4 | adantr 482 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β ( I βΎ π) β πΈ) |
12 | | simpr 486 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β π’ β πΈ) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ·) = (.rβπ·) |
14 | 1, 2, 3, 5, 13 | erngmul 39319 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π) β πΈ β§ π’ β πΈ)) β (( I βΎ π)(.rβπ·)π’) = (( I βΎ π) β π’)) |
15 | 10, 11, 12, 14 | syl12anc 836 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (( I βΎ π)(.rβπ·)π’) = (( I βΎ π) β π’)) |
16 | 1, 2, 3 | tendo1mul 39283 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (( I βΎ π) β π’) = π’) |
17 | 15, 16 | eqtrd 2773 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (( I βΎ π)(.rβπ·)π’) = π’) |
18 | 1, 2, 3, 5, 13 | erngmul 39319 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π’ β πΈ β§ ( I βΎ π) β πΈ)) β (π’(.rβπ·)( I βΎ π)) = (π’ β ( I βΎ π))) |
19 | 10, 12, 11, 18 | syl12anc 836 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (π’(.rβπ·)( I βΎ π)) = (π’ β ( I βΎ π))) |
20 | 1, 2, 3 | tendo1mulr 39284 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (π’ β ( I βΎ π)) = π’) |
21 | 19, 20 | eqtrd 2773 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β (π’(.rβπ·)( I βΎ π)) = π’) |
22 | 17, 21 | jca 513 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π’ β πΈ) β ((( I βΎ π)(.rβπ·)π’) = π’ β§ (π’(.rβπ·)( I βΎ π)) = π’)) |
23 | 22 | ex 414 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (π’ β πΈ β ((( I βΎ π)(.rβπ·)π’) = π’ β§ (π’(.rβπ·)( I βΎ π)) = π’))) |
24 | 9, 23 | sylbid 239 |
. . 3
β’ ((πΎ β HL β§ π β π») β (π’ β (Baseβπ·) β ((( I βΎ π)(.rβπ·)π’) = π’ β§ (π’(.rβπ·)( I βΎ π)) = π’))) |
25 | 24 | ralrimiv 3139 |
. 2
β’ ((πΎ β HL β§ π β π») β βπ’ β (Baseβπ·)((( I βΎ π)(.rβπ·)π’) = π’ β§ (π’(.rβπ·)( I βΎ π)) = π’)) |
26 | | erng1.r |
. . 3
β’ ((πΎ β HL β§ π β π») β π· β Ring) |
27 | | eqid 2733 |
. . . 4
β’
(1rβπ·) = (1rβπ·) |
28 | 6, 13, 27 | isringid 20002 |
. . 3
β’ (π· β Ring β ((( I
βΎ π) β
(Baseβπ·) β§
βπ’ β
(Baseβπ·)((( I βΎ
π)(.rβπ·)π’) = π’ β§ (π’(.rβπ·)( I βΎ π)) = π’)) β (1rβπ·) = ( I βΎ π))) |
29 | 26, 28 | syl 17 |
. 2
β’ ((πΎ β HL β§ π β π») β ((( I βΎ π) β (Baseβπ·) β§ βπ’ β (Baseβπ·)((( I βΎ π)(.rβπ·)π’) = π’ β§ (π’(.rβπ·)( I βΎ π)) = π’)) β (1rβπ·) = ( I βΎ π))) |
30 | 8, 25, 29 | mpbi2and 711 |
1
β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) |