Step | Hyp | Ref
| Expression |
1 | | srhmsubc.c |
. . . 4
β’ πΆ = (π β© π) |
2 | | eleq1w 2810 |
. . . . . . 7
β’ (π = π₯ β (π β Ring β π₯ β Ring)) |
3 | | srhmsubc.s |
. . . . . . 7
β’
βπ β
π π β Ring |
4 | 2, 3 | vtoclri 3570 |
. . . . . 6
β’ (π₯ β π β π₯ β Ring) |
5 | 4 | ssriv 3981 |
. . . . 5
β’ π β Ring |
6 | | sslin 4229 |
. . . . 5
β’ (π β Ring β (π β© π) β (π β© Ring)) |
7 | 5, 6 | mp1i 13 |
. . . 4
β’ (π β π β (π β© π) β (π β© Ring)) |
8 | 1, 7 | eqsstrid 4025 |
. . 3
β’ (π β π β πΆ β (π β© Ring)) |
9 | | ssid 3999 |
. . . . . 6
β’ (π₯ RingHom π¦) β (π₯ RingHom π¦) |
10 | | eqid 2726 |
. . . . . . 7
β’
(RingCatβπ) =
(RingCatβπ) |
11 | | eqid 2726 |
. . . . . . 7
β’
(Baseβ(RingCatβπ)) = (Baseβ(RingCatβπ)) |
12 | | simpl 482 |
. . . . . . 7
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β π β π) |
13 | | eqid 2726 |
. . . . . . 7
β’ (Hom
β(RingCatβπ)) =
(Hom β(RingCatβπ)) |
14 | 3, 1 | srhmsubclem2 20574 |
. . . . . . . 8
β’ ((π β π β§ π₯ β πΆ) β π₯ β (Baseβ(RingCatβπ))) |
15 | 14 | adantrr 714 |
. . . . . . 7
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β π₯ β (Baseβ(RingCatβπ))) |
16 | 3, 1 | srhmsubclem2 20574 |
. . . . . . . 8
β’ ((π β π β§ π¦ β πΆ) β π¦ β (Baseβ(RingCatβπ))) |
17 | 16 | adantrl 713 |
. . . . . . 7
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β π¦ β (Baseβ(RingCatβπ))) |
18 | 10, 11, 12, 13, 15, 17 | ringchom 20548 |
. . . . . 6
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(Hom β(RingCatβπ))π¦) = (π₯ RingHom π¦)) |
19 | 9, 18 | sseqtrrid 4030 |
. . . . 5
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ RingHom π¦) β (π₯(Hom β(RingCatβπ))π¦)) |
20 | | srhmsubc.j |
. . . . . . 7
β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) |
21 | 20 | a1i 11 |
. . . . . 6
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β π½ = (π β πΆ, π β πΆ β¦ (π RingHom π ))) |
22 | | oveq12 7414 |
. . . . . . 7
β’ ((π = π₯ β§ π = π¦) β (π RingHom π ) = (π₯ RingHom π¦)) |
23 | 22 | adantl 481 |
. . . . . 6
β’ (((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β§ (π = π₯ β§ π = π¦)) β (π RingHom π ) = (π₯ RingHom π¦)) |
24 | | simprl 768 |
. . . . . 6
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β π₯ β πΆ) |
25 | | simprr 770 |
. . . . . 6
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β π¦ β πΆ) |
26 | | ovexd 7440 |
. . . . . 6
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ RingHom π¦) β V) |
27 | 21, 23, 24, 25, 26 | ovmpod 7556 |
. . . . 5
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯π½π¦) = (π₯ RingHom π¦)) |
28 | | eqid 2726 |
. . . . . 6
β’
(Homf β(RingCatβπ)) = (Homf
β(RingCatβπ)) |
29 | 28, 11, 13, 15, 17 | homfval 17645 |
. . . . 5
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(Homf
β(RingCatβπ))π¦) = (π₯(Hom β(RingCatβπ))π¦)) |
30 | 19, 27, 29 | 3sstr4d 4024 |
. . . 4
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯π½π¦) β (π₯(Homf
β(RingCatβπ))π¦)) |
31 | 30 | ralrimivva 3194 |
. . 3
β’ (π β π β βπ₯ β πΆ βπ¦ β πΆ (π₯π½π¦) β (π₯(Homf
β(RingCatβπ))π¦)) |
32 | | ovex 7438 |
. . . . . 6
β’ (π RingHom π ) β V |
33 | 20, 32 | fnmpoi 8055 |
. . . . 5
β’ π½ Fn (πΆ Γ πΆ) |
34 | 33 | a1i 11 |
. . . 4
β’ (π β π β π½ Fn (πΆ Γ πΆ)) |
35 | 28, 11 | homffn 17646 |
. . . . 5
β’
(Homf β(RingCatβπ)) Fn ((Baseβ(RingCatβπ)) Γ
(Baseβ(RingCatβπ))) |
36 | | id 22 |
. . . . . . . . 9
β’ (π β π β π β π) |
37 | 10, 11, 36 | ringcbas 20546 |
. . . . . . . 8
β’ (π β π β (Baseβ(RingCatβπ)) = (π β© Ring)) |
38 | 37 | eqcomd 2732 |
. . . . . . 7
β’ (π β π β (π β© Ring) =
(Baseβ(RingCatβπ))) |
39 | 38 | sqxpeqd 5701 |
. . . . . 6
β’ (π β π β ((π β© Ring) Γ (π β© Ring)) =
((Baseβ(RingCatβπ)) Γ (Baseβ(RingCatβπ)))) |
40 | 39 | fneq2d 6637 |
. . . . 5
β’ (π β π β ((Homf
β(RingCatβπ))
Fn ((π β© Ring) Γ
(π β© Ring)) β
(Homf β(RingCatβπ)) Fn ((Baseβ(RingCatβπ)) Γ
(Baseβ(RingCatβπ))))) |
41 | 35, 40 | mpbiri 258 |
. . . 4
β’ (π β π β (Homf
β(RingCatβπ))
Fn ((π β© Ring) Γ
(π β©
Ring))) |
42 | | inex1g 5312 |
. . . 4
β’ (π β π β (π β© Ring) β V) |
43 | 34, 41, 42 | isssc 17776 |
. . 3
β’ (π β π β (π½ βcat
(Homf β(RingCatβπ)) β (πΆ β (π β© Ring) β§ βπ₯ β πΆ βπ¦ β πΆ (π₯π½π¦) β (π₯(Homf
β(RingCatβπ))π¦)))) |
44 | 8, 31, 43 | mpbir2and 710 |
. 2
β’ (π β π β π½ βcat
(Homf β(RingCatβπ))) |
45 | 1 | elin2 4192 |
. . . . . . . 8
β’ (π₯ β πΆ β (π₯ β π β§ π₯ β π)) |
46 | 4 | adantl 481 |
. . . . . . . 8
β’ ((π₯ β π β§ π₯ β π) β π₯ β Ring) |
47 | 45, 46 | sylbi 216 |
. . . . . . 7
β’ (π₯ β πΆ β π₯ β Ring) |
48 | 47 | adantl 481 |
. . . . . 6
β’ ((π β π β§ π₯ β πΆ) β π₯ β Ring) |
49 | | eqid 2726 |
. . . . . . 7
β’
(Baseβπ₯) =
(Baseβπ₯) |
50 | 49 | idrhm 20392 |
. . . . . 6
β’ (π₯ β Ring β ( I βΎ
(Baseβπ₯)) β
(π₯ RingHom π₯)) |
51 | 48, 50 | syl 17 |
. . . . 5
β’ ((π β π β§ π₯ β πΆ) β ( I βΎ (Baseβπ₯)) β (π₯ RingHom π₯)) |
52 | | eqid 2726 |
. . . . . 6
β’
(Idβ(RingCatβπ)) = (Idβ(RingCatβπ)) |
53 | | simpl 482 |
. . . . . 6
β’ ((π β π β§ π₯ β πΆ) β π β π) |
54 | 10, 11, 52, 53, 14, 49 | ringcid 20560 |
. . . . 5
β’ ((π β π β§ π₯ β πΆ) β ((Idβ(RingCatβπ))βπ₯) = ( I βΎ (Baseβπ₯))) |
55 | 20 | a1i 11 |
. . . . . 6
β’ ((π β π β§ π₯ β πΆ) β π½ = (π β πΆ, π β πΆ β¦ (π RingHom π ))) |
56 | | oveq12 7414 |
. . . . . . 7
β’ ((π = π₯ β§ π = π₯) β (π RingHom π ) = (π₯ RingHom π₯)) |
57 | 56 | adantl 481 |
. . . . . 6
β’ (((π β π β§ π₯ β πΆ) β§ (π = π₯ β§ π = π₯)) β (π RingHom π ) = (π₯ RingHom π₯)) |
58 | | simpr 484 |
. . . . . 6
β’ ((π β π β§ π₯ β πΆ) β π₯ β πΆ) |
59 | | ovexd 7440 |
. . . . . 6
β’ ((π β π β§ π₯ β πΆ) β (π₯ RingHom π₯) β V) |
60 | 55, 57, 58, 58, 59 | ovmpod 7556 |
. . . . 5
β’ ((π β π β§ π₯ β πΆ) β (π₯π½π₯) = (π₯ RingHom π₯)) |
61 | 51, 54, 60 | 3eltr4d 2842 |
. . . 4
β’ ((π β π β§ π₯ β πΆ) β ((Idβ(RingCatβπ))βπ₯) β (π₯π½π₯)) |
62 | | eqid 2726 |
. . . . . . . . 9
β’
(compβ(RingCatβπ)) = (compβ(RingCatβπ)) |
63 | 10 | ringccat 20559 |
. . . . . . . . . 10
β’ (π β π β (RingCatβπ) β Cat) |
64 | 63 | ad3antrrr 727 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (RingCatβπ) β Cat) |
65 | 14 | adantr 480 |
. . . . . . . . . 10
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π₯ β (Baseβ(RingCatβπ))) |
66 | 65 | adantr 480 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β π₯ β (Baseβ(RingCatβπ))) |
67 | 16 | ad2ant2r 744 |
. . . . . . . . . 10
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π¦ β (Baseβ(RingCatβπ))) |
68 | 67 | adantr 480 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β π¦ β (Baseβ(RingCatβπ))) |
69 | 3, 1 | srhmsubclem2 20574 |
. . . . . . . . . . 11
β’ ((π β π β§ π§ β πΆ) β π§ β (Baseβ(RingCatβπ))) |
70 | 69 | ad2ant2rl 746 |
. . . . . . . . . 10
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π§ β (Baseβ(RingCatβπ))) |
71 | 70 | adantr 480 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β π§ β (Baseβ(RingCatβπ))) |
72 | 53 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π β π) |
73 | | simpl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β πΆ β§ π§ β πΆ) β π¦ β πΆ) |
74 | 58, 73 | anim12i 612 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π₯ β πΆ β§ π¦ β πΆ)) |
75 | 72, 74 | jca 511 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π β π β§ (π₯ β πΆ β§ π¦ β πΆ))) |
76 | 3, 1, 20 | srhmsubclem3 20575 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯π½π¦) = (π₯(Hom β(RingCatβπ))π¦)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π₯π½π¦) = (π₯(Hom β(RingCatβπ))π¦)) |
78 | 77 | eleq2d 2813 |
. . . . . . . . . . . 12
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π β (π₯π½π¦) β π β (π₯(Hom β(RingCatβπ))π¦))) |
79 | 78 | biimpcd 248 |
. . . . . . . . . . 11
β’ (π β (π₯π½π¦) β (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π β (π₯(Hom β(RingCatβπ))π¦))) |
80 | 79 | adantr 480 |
. . . . . . . . . 10
β’ ((π β (π₯π½π¦) β§ π β (π¦π½π§)) β (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π β (π₯(Hom β(RingCatβπ))π¦))) |
81 | 80 | impcom 407 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β π β (π₯(Hom β(RingCatβπ))π¦)) |
82 | 3, 1, 20 | srhmsubclem3 20575 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ (π¦ β πΆ β§ π§ β πΆ)) β (π¦π½π§) = (π¦(Hom β(RingCatβπ))π§)) |
83 | 82 | adantlr 712 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π¦π½π§) = (π¦(Hom β(RingCatβπ))π§)) |
84 | 83 | eleq2d 2813 |
. . . . . . . . . . . 12
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π β (π¦π½π§) β π β (π¦(Hom β(RingCatβπ))π§))) |
85 | 84 | biimpd 228 |
. . . . . . . . . . 11
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π β (π¦π½π§) β π β (π¦(Hom β(RingCatβπ))π§))) |
86 | 85 | adantld 490 |
. . . . . . . . . 10
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β ((π β (π₯π½π¦) β§ π β (π¦π½π§)) β π β (π¦(Hom β(RingCatβπ))π§))) |
87 | 86 | imp 406 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β π β (π¦(Hom β(RingCatβπ))π§)) |
88 | 11, 13, 62, 64, 66, 68, 71, 81, 87 | catcocl 17638 |
. . . . . . . 8
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯(Hom β(RingCatβπ))π§)) |
89 | 10, 11, 72, 13, 65, 70 | ringchom 20548 |
. . . . . . . . . 10
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π₯(Hom β(RingCatβπ))π§) = (π₯ RingHom π§)) |
90 | 89 | eqcomd 2732 |
. . . . . . . . 9
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π₯ RingHom π§) = (π₯(Hom β(RingCatβπ))π§)) |
91 | 90 | adantr 480 |
. . . . . . . 8
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (π₯ RingHom π§) = (π₯(Hom β(RingCatβπ))π§)) |
92 | 88, 91 | eleqtrrd 2830 |
. . . . . . 7
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯ RingHom π§)) |
93 | 20 | a1i 11 |
. . . . . . . . 9
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π½ = (π β πΆ, π β πΆ β¦ (π RingHom π ))) |
94 | | oveq12 7414 |
. . . . . . . . . 10
β’ ((π = π₯ β§ π = π§) β (π RingHom π ) = (π₯ RingHom π§)) |
95 | 94 | adantl 481 |
. . . . . . . . 9
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π = π₯ β§ π = π§)) β (π RingHom π ) = (π₯ RingHom π§)) |
96 | 58 | adantr 480 |
. . . . . . . . 9
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π₯ β πΆ) |
97 | | simprr 770 |
. . . . . . . . 9
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β π§ β πΆ) |
98 | | ovexd 7440 |
. . . . . . . . 9
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π₯ RingHom π§) β V) |
99 | 93, 95, 96, 97, 98 | ovmpod 7556 |
. . . . . . . 8
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β (π₯π½π§) = (π₯ RingHom π§)) |
100 | 99 | adantr 480 |
. . . . . . 7
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (π₯π½π§) = (π₯ RingHom π§)) |
101 | 92, 100 | eleqtrrd 2830 |
. . . . . 6
β’ ((((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯π½π§)) |
102 | 101 | ralrimivva 3194 |
. . . . 5
β’ (((π β π β§ π₯ β πΆ) β§ (π¦ β πΆ β§ π§ β πΆ)) β βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯π½π§)) |
103 | 102 | ralrimivva 3194 |
. . . 4
β’ ((π β π β§ π₯ β πΆ) β βπ¦ β πΆ βπ§ β πΆ βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯π½π§)) |
104 | 61, 103 | jca 511 |
. . 3
β’ ((π β π β§ π₯ β πΆ) β (((Idβ(RingCatβπ))βπ₯) β (π₯π½π₯) β§ βπ¦ β πΆ βπ§ β πΆ βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯π½π§))) |
105 | 104 | ralrimiva 3140 |
. 2
β’ (π β π β βπ₯ β πΆ (((Idβ(RingCatβπ))βπ₯) β (π₯π½π₯) β§ βπ¦ β πΆ βπ§ β πΆ βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯π½π§))) |
106 | 28, 52, 62, 63, 34 | issubc2 17795 |
. 2
β’ (π β π β (π½ β (Subcatβ(RingCatβπ)) β (π½ βcat
(Homf β(RingCatβπ)) β§ βπ₯ β πΆ (((Idβ(RingCatβπ))βπ₯) β (π₯π½π₯) β§ βπ¦ β πΆ βπ§ β πΆ βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβ(RingCatβπ))π§)π) β (π₯π½π§))))) |
107 | 44, 105, 106 | mpbir2and 710 |
1
β’ (π β π β π½ β (Subcatβ(RingCatβπ))) |