Step | Hyp | Ref
| Expression |
1 | | rhmsubcsetc.b |
. . . . . 6
β’ (π β π΅ = (Ring β© π)) |
2 | 1 | eleq2d 2824 |
. . . . 5
β’ (π β (π₯ β π΅ β π₯ β (Ring β© π))) |
3 | | elin 3931 |
. . . . . 6
β’ (π₯ β (Ring β© π) β (π₯ β Ring β§ π₯ β π)) |
4 | 3 | simplbi 499 |
. . . . 5
β’ (π₯ β (Ring β© π) β π₯ β Ring) |
5 | 2, 4 | syl6bi 253 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β Ring)) |
6 | 5 | imp 408 |
. . 3
β’ ((π β§ π₯ β π΅) β π₯ β Ring) |
7 | | eqid 2737 |
. . . 4
β’
(Baseβπ₯) =
(Baseβπ₯) |
8 | 7 | idrhm 20172 |
. . 3
β’ (π₯ β Ring β ( I βΎ
(Baseβπ₯)) β
(π₯ RingHom π₯)) |
9 | 6, 8 | syl 17 |
. 2
β’ ((π β§ π₯ β π΅) β ( I βΎ (Baseβπ₯)) β (π₯ RingHom π₯)) |
10 | | rhmsubcsetc.c |
. . 3
β’ πΆ = (ExtStrCatβπ) |
11 | | eqid 2737 |
. . 3
β’
(IdβπΆ) =
(IdβπΆ) |
12 | | rhmsubcsetc.u |
. . . 4
β’ (π β π β π) |
13 | 12 | adantr 482 |
. . 3
β’ ((π β§ π₯ β π΅) β π β π) |
14 | 3 | simprbi 498 |
. . . . 5
β’ (π₯ β (Ring β© π) β π₯ β π) |
15 | 2, 14 | syl6bi 253 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β π)) |
16 | 15 | imp 408 |
. . 3
β’ ((π β§ π₯ β π΅) β π₯ β π) |
17 | 10, 11, 13, 16 | estrcid 18028 |
. 2
β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) = ( I βΎ (Baseβπ₯))) |
18 | | rhmsubcsetc.h |
. . . 4
β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) |
19 | 18 | oveqdr 7390 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯π»π₯) = (π₯( RingHom βΎ (π΅ Γ π΅))π₯)) |
20 | | eqid 2737 |
. . . . . . . 8
β’
(RingCatβπ) =
(RingCatβπ) |
21 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(RingCatβπ)) = (Baseβ(RingCatβπ)) |
22 | | eqid 2737 |
. . . . . . . 8
β’ (Hom
β(RingCatβπ)) =
(Hom β(RingCatβπ)) |
23 | 20, 21, 12, 22 | ringchomfval 46384 |
. . . . . . 7
β’ (π β (Hom
β(RingCatβπ)) =
( RingHom βΎ ((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ))))) |
24 | 20, 21, 12 | ringcbas 46383 |
. . . . . . . . . 10
β’ (π β
(Baseβ(RingCatβπ)) = (π β© Ring)) |
25 | | incom 4166 |
. . . . . . . . . . . 12
β’ (Ring
β© π) = (π β© Ring) |
26 | 1, 25 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π β π΅ = (π β© Ring)) |
27 | 26 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β (π β© Ring) = π΅) |
28 | 24, 27 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β
(Baseβ(RingCatβπ)) = π΅) |
29 | 28 | sqxpeqd 5670 |
. . . . . . . 8
β’ (π β
((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ))) = (π΅ Γ π΅)) |
30 | 29 | reseq2d 5942 |
. . . . . . 7
β’ (π β ( RingHom βΎ
((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ)))) = ( RingHom βΎ (π΅ Γ π΅))) |
31 | 23, 30 | eqtrd 2777 |
. . . . . 6
β’ (π β (Hom
β(RingCatβπ)) =
( RingHom βΎ (π΅
Γ π΅))) |
32 | 31 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (Hom β(RingCatβπ)) = ( RingHom βΎ (π΅ Γ π΅))) |
33 | 32 | eqcomd 2743 |
. . . 4
β’ ((π β§ π₯ β π΅) β ( RingHom βΎ (π΅ Γ π΅)) = (Hom β(RingCatβπ))) |
34 | 33 | oveqd 7379 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯( RingHom βΎ (π΅ Γ π΅))π₯) = (π₯(Hom β(RingCatβπ))π₯)) |
35 | 26 | eleq2d 2824 |
. . . . . 6
β’ (π β (π₯ β π΅ β π₯ β (π β© Ring))) |
36 | 35 | biimpa 478 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π₯ β (π β© Ring)) |
37 | 24 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (Baseβ(RingCatβπ)) = (π β© Ring)) |
38 | 36, 37 | eleqtrrd 2841 |
. . . 4
β’ ((π β§ π₯ β π΅) β π₯ β (Baseβ(RingCatβπ))) |
39 | 20, 21, 13, 22, 38, 38 | ringchom 46385 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯(Hom β(RingCatβπ))π₯) = (π₯ RingHom π₯)) |
40 | 19, 34, 39 | 3eqtrd 2781 |
. 2
β’ ((π β§ π₯ β π΅) β (π₯π»π₯) = (π₯ RingHom π₯)) |
41 | 9, 17, 40 | 3eltr4d 2853 |
1
β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) |