Step | Hyp | Ref
| Expression |
1 | | rngcrescrhm.u |
. . . 4
β’ (π β π β π) |
2 | | rngcrescrhm.r |
. . . 4
β’ (π β π
= (Ring β© π)) |
3 | | eqidd 2739 |
. . . 4
β’ (π β (Rng β© π) = (Rng β© π)) |
4 | 1, 2, 3 | rhmsscrnghm 46042 |
. . 3
β’ (π β ( RingHom βΎ (π
Γ π
)) βcat ( RngHomo βΎ
((Rng β© π) Γ (Rng
β© π)))) |
5 | | rngcrescrhm.h |
. . . 4
β’ π» = ( RingHom βΎ (π
Γ π
)) |
6 | 5 | a1i 11 |
. . 3
β’ (π β π» = ( RingHom βΎ (π
Γ π
))) |
7 | | rngcrescrhm.c |
. . . . . . 7
β’ πΆ = (RngCatβπ) |
8 | 7 | a1i 11 |
. . . . . 6
β’ (π β πΆ = (RngCatβπ)) |
9 | 8 | eqcomd 2744 |
. . . . 5
β’ (π β (RngCatβπ) = πΆ) |
10 | 9 | fveq2d 6842 |
. . . 4
β’ (π β (Homf
β(RngCatβπ)) =
(Homf βπΆ)) |
11 | | eqid 2738 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
12 | 7, 11, 1 | rngchomfeqhom 45985 |
. . . 4
β’ (π β (Homf
βπΆ) = (Hom
βπΆ)) |
13 | | eqid 2738 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
14 | 7, 11, 1, 13 | rngchomfval 45982 |
. . . . 5
β’ (π β (Hom βπΆ) = ( RngHomo βΎ
((BaseβπΆ) Γ
(BaseβπΆ)))) |
15 | 7, 11, 1 | rngcbas 45981 |
. . . . . . . 8
β’ (π β (BaseβπΆ) = (π β© Rng)) |
16 | | incom 4160 |
. . . . . . . 8
β’ (π β© Rng) = (Rng β© π) |
17 | 15, 16 | eqtrdi 2794 |
. . . . . . 7
β’ (π β (BaseβπΆ) = (Rng β© π)) |
18 | 17 | sqxpeqd 5663 |
. . . . . 6
β’ (π β ((BaseβπΆ) Γ (BaseβπΆ)) = ((Rng β© π) Γ (Rng β© π))) |
19 | 18 | reseq2d 5934 |
. . . . 5
β’ (π β ( RngHomo βΎ
((BaseβπΆ) Γ
(BaseβπΆ))) = (
RngHomo βΎ ((Rng β© π) Γ (Rng β© π)))) |
20 | 14, 19 | eqtrd 2778 |
. . . 4
β’ (π β (Hom βπΆ) = ( RngHomo βΎ ((Rng
β© π) Γ (Rng β©
π)))) |
21 | 10, 12, 20 | 3eqtrd 2782 |
. . 3
β’ (π β (Homf
β(RngCatβπ)) =
( RngHomo βΎ ((Rng β© π) Γ (Rng β© π)))) |
22 | 4, 6, 21 | 3brtr4d 5136 |
. 2
β’ (π β π» βcat
(Homf β(RngCatβπ))) |
23 | 1, 7, 2, 5 | rhmsubclem3 46104 |
. . . 4
β’ ((π β§ π₯ β π
) β ((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯)) |
24 | 1, 7, 2, 5 | rhmsubclem4 46105 |
. . . . . 6
β’ ((((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) |
25 | 24 | ralrimivva 3196 |
. . . . 5
β’ (((π β§ π₯ β π
) β§ (π¦ β π
β§ π§ β π
)) β βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) |
26 | 25 | ralrimivva 3196 |
. . . 4
β’ ((π β§ π₯ β π
) β βπ¦ β π
βπ§ β π
βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§)) |
27 | 23, 26 | jca 513 |
. . 3
β’ ((π β§ π₯ β π
) β (((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯) β§ βπ¦ β π
βπ§ β π
βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§))) |
28 | 27 | ralrimiva 3142 |
. 2
β’ (π β βπ₯ β π
(((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯) β§ βπ¦ β π
βπ§ β π
βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§))) |
29 | | eqid 2738 |
. . 3
β’
(Homf β(RngCatβπ)) = (Homf
β(RngCatβπ)) |
30 | | eqid 2738 |
. . 3
β’
(Idβ(RngCatβπ)) = (Idβ(RngCatβπ)) |
31 | | eqid 2738 |
. . 3
β’
(compβ(RngCatβπ)) = (compβ(RngCatβπ)) |
32 | | eqid 2738 |
. . . . 5
β’
(RngCatβπ) =
(RngCatβπ) |
33 | 32 | rngccat 45994 |
. . . 4
β’ (π β π β (RngCatβπ) β Cat) |
34 | 1, 33 | syl 17 |
. . 3
β’ (π β (RngCatβπ) β Cat) |
35 | 1, 7, 2, 5 | rhmsubclem1 46102 |
. . 3
β’ (π β π» Fn (π
Γ π
)) |
36 | 29, 30, 31, 34, 35 | issubc2 17657 |
. 2
β’ (π β (π» β (Subcatβ(RngCatβπ)) β (π» βcat
(Homf β(RngCatβπ)) β§ βπ₯ β π
(((Idβ(RngCatβπ))βπ₯) β (π₯π»π₯) β§ βπ¦ β π
βπ§ β π
βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβ(RngCatβπ))π§)π) β (π₯π»π§))))) |
37 | 22, 28, 36 | mpbir2and 712 |
1
β’ (π β π» β (Subcatβ(RngCatβπ))) |