Step | Hyp | Ref
| Expression |
1 | | rhmsubcrngc.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 | | rhmsubcrngc.c |
. . 3
β’ πΆ = (RngCatβπ) |
11 | | eqid 2737 |
. . 3
β’
(BaseβπΆ) =
(BaseβπΆ) |
12 | | eqid 2737 |
. . 3
β’
(IdβπΆ) =
(IdβπΆ) |
13 | | rhmsubcrngc.u |
. . . 4
β’ (π β π β π) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ π₯ β π΅) β π β π) |
15 | | ringrng 46251 |
. . . . . . . . . . . 12
β’ (π₯ β Ring β π₯ β Rng) |
16 | 15 | anim2i 618 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π₯ β Ring) β (π₯ β π β§ π₯ β Rng)) |
17 | 16 | ancoms 460 |
. . . . . . . . . 10
β’ ((π₯ β Ring β§ π₯ β π) β (π₯ β π β§ π₯ β Rng)) |
18 | 3, 17 | sylbi 216 |
. . . . . . . . 9
β’ (π₯ β (Ring β© π) β (π₯ β π β§ π₯ β Rng)) |
19 | 18 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (Ring β© π)) β (π₯ β π β§ π₯ β Rng)) |
20 | | elin 3931 |
. . . . . . . 8
β’ (π₯ β (π β© Rng) β (π₯ β π β§ π₯ β Rng)) |
21 | 19, 20 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π₯ β (Ring β© π)) β π₯ β (π β© Rng)) |
22 | 10, 11, 13 | rngcbas 46337 |
. . . . . . . 8
β’ (π β (BaseβπΆ) = (π β© Rng)) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Ring β© π)) β (BaseβπΆ) = (π β© Rng)) |
24 | 21, 23 | eleqtrrd 2841 |
. . . . . 6
β’ ((π β§ π₯ β (Ring β© π)) β π₯ β (BaseβπΆ)) |
25 | 24 | ex 414 |
. . . . 5
β’ (π β (π₯ β (Ring β© π) β π₯ β (BaseβπΆ))) |
26 | 2, 25 | sylbid 239 |
. . . 4
β’ (π β (π₯ β π΅ β π₯ β (BaseβπΆ))) |
27 | 26 | imp 408 |
. . 3
β’ ((π β§ π₯ β π΅) β π₯ β (BaseβπΆ)) |
28 | 10, 11, 12, 14, 27, 7 | rngcid 46351 |
. 2
β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) = ( I βΎ (Baseβπ₯))) |
29 | | rhmsubcrngc.h |
. . . 4
β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) |
30 | 29 | oveqdr 7390 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯π»π₯) = (π₯( RingHom βΎ (π΅ Γ π΅))π₯)) |
31 | | eqid 2737 |
. . . . . . . 8
β’
(RingCatβπ) =
(RingCatβπ) |
32 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(RingCatβπ)) = (Baseβ(RingCatβπ)) |
33 | | eqid 2737 |
. . . . . . . 8
β’ (Hom
β(RingCatβπ)) =
(Hom β(RingCatβπ)) |
34 | 31, 32, 13, 33 | ringchomfval 46384 |
. . . . . . 7
β’ (π β (Hom
β(RingCatβπ)) =
( RingHom βΎ ((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ))))) |
35 | 31, 32, 13 | ringcbas 46383 |
. . . . . . . . . 10
β’ (π β
(Baseβ(RingCatβπ)) = (π β© Ring)) |
36 | | incom 4166 |
. . . . . . . . . . . 12
β’ (Ring
β© π) = (π β© Ring) |
37 | 1, 36 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π β π΅ = (π β© Ring)) |
38 | 37 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π β (π β© Ring) = π΅) |
39 | 35, 38 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β
(Baseβ(RingCatβπ)) = π΅) |
40 | 39 | sqxpeqd 5670 |
. . . . . . . 8
β’ (π β
((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ))) = (π΅ Γ π΅)) |
41 | 40 | reseq2d 5942 |
. . . . . . 7
β’ (π β ( RingHom βΎ
((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ)))) = ( RingHom βΎ (π΅ Γ π΅))) |
42 | 34, 41 | eqtrd 2777 |
. . . . . 6
β’ (π β (Hom
β(RingCatβπ)) =
( RingHom βΎ (π΅
Γ π΅))) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (Hom β(RingCatβπ)) = ( RingHom βΎ (π΅ Γ π΅))) |
44 | 43 | eqcomd 2743 |
. . . 4
β’ ((π β§ π₯ β π΅) β ( RingHom βΎ (π΅ Γ π΅)) = (Hom β(RingCatβπ))) |
45 | 44 | oveqd 7379 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯( RingHom βΎ (π΅ Γ π΅))π₯) = (π₯(Hom β(RingCatβπ))π₯)) |
46 | 37 | eleq2d 2824 |
. . . . . 6
β’ (π β (π₯ β π΅ β π₯ β (π β© Ring))) |
47 | 46 | biimpa 478 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π₯ β (π β© Ring)) |
48 | 35 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (Baseβ(RingCatβπ)) = (π β© Ring)) |
49 | 47, 48 | eleqtrrd 2841 |
. . . 4
β’ ((π β§ π₯ β π΅) β π₯ β (Baseβ(RingCatβπ))) |
50 | 31, 32, 14, 33, 49, 49 | ringchom 46385 |
. . 3
β’ ((π β§ π₯ β π΅) β (π₯(Hom β(RingCatβπ))π₯) = (π₯ RingHom π₯)) |
51 | 30, 45, 50 | 3eqtrd 2781 |
. 2
β’ ((π β§ π₯ β π΅) β (π₯π»π₯) = (π₯ RingHom π₯)) |
52 | 9, 28, 51 | 3eltr4d 2853 |
1
β’ ((π β§ π₯ β π΅) β ((IdβπΆ)βπ₯) β (π₯π»π₯)) |