Step | Hyp | Ref
| Expression |
1 | | zex 12515 |
. . . . . 6
β’ β€
β V |
2 | 1 | mptex 7178 |
. . . . 5
β’ (π§ β β€ β¦ (π§(.gβπ)(1rβπ))) β V |
3 | | irinitoringc.c |
. . . . . . . . 9
β’ πΆ = (RingCatβπ) |
4 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΆ) =
(BaseβπΆ) |
5 | | irinitoringc.u |
. . . . . . . . 9
β’ (π β π β π) |
6 | | eqid 2737 |
. . . . . . . . 9
β’ (Hom
βπΆ) = (Hom
βπΆ) |
7 | 3, 4, 5, 6 | ringchomfval 46384 |
. . . . . . . 8
β’ (π β (Hom βπΆ) = ( RingHom βΎ
((BaseβπΆ) Γ
(BaseβπΆ)))) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (BaseβπΆ)) β (Hom βπΆ) = ( RingHom βΎ ((BaseβπΆ) Γ (BaseβπΆ)))) |
9 | 8 | oveqd 7379 |
. . . . . 6
β’ ((π β§ π β (BaseβπΆ)) β (β€ring(Hom
βπΆ)π) = (β€ring( RingHom βΎ
((BaseβπΆ) Γ
(BaseβπΆ)))π)) |
10 | | irinitoringc.z |
. . . . . . . . . 10
β’ (π β β€ring
β π) |
11 | | id 22 |
. . . . . . . . . . 11
β’
(β€ring β π β β€ring β π) |
12 | | zringring 20888 |
. . . . . . . . . . . 12
β’
β€ring β Ring |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
β’
(β€ring β π β β€ring β
Ring) |
14 | 11, 13 | elind 4159 |
. . . . . . . . . 10
β’
(β€ring β π β β€ring β (π β© Ring)) |
15 | 10, 14 | syl 17 |
. . . . . . . . 9
β’ (π β β€ring
β (π β©
Ring)) |
16 | 3, 4, 5 | ringcbas 46383 |
. . . . . . . . 9
β’ (π β (BaseβπΆ) = (π β© Ring)) |
17 | 15, 16 | eleqtrrd 2841 |
. . . . . . . 8
β’ (π β β€ring
β (BaseβπΆ)) |
18 | 17 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (BaseβπΆ)) β β€ring β
(BaseβπΆ)) |
19 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
20 | 18, 19 | ovresd 7526 |
. . . . . 6
β’ ((π β§ π β (BaseβπΆ)) β (β€ring( RingHom
βΎ ((BaseβπΆ)
Γ (BaseβπΆ)))π) = (β€ring RingHom π)) |
21 | 16 | eleq2d 2824 |
. . . . . . . . 9
β’ (π β (π β (BaseβπΆ) β π β (π β© Ring))) |
22 | | elin 3931 |
. . . . . . . . . 10
β’ (π β (π β© Ring) β (π β π β§ π β Ring)) |
23 | 22 | simprbi 498 |
. . . . . . . . 9
β’ (π β (π β© Ring) β π β Ring) |
24 | 21, 23 | syl6bi 253 |
. . . . . . . 8
β’ (π β (π β (BaseβπΆ) β π β Ring)) |
25 | 24 | imp 408 |
. . . . . . 7
β’ ((π β§ π β (BaseβπΆ)) β π β Ring) |
26 | | eqid 2737 |
. . . . . . . 8
β’
(.gβπ) = (.gβπ) |
27 | | eqid 2737 |
. . . . . . . 8
β’ (π§ β β€ β¦ (π§(.gβπ)(1rβπ))) = (π§ β β€ β¦ (π§(.gβπ)(1rβπ))) |
28 | | eqid 2737 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
29 | 26, 27, 28 | mulgrhm2 20915 |
. . . . . . 7
β’ (π β Ring β
(β€ring RingHom π) = {(π§ β β€ β¦ (π§(.gβπ)(1rβπ)))}) |
30 | 25, 29 | syl 17 |
. . . . . 6
β’ ((π β§ π β (BaseβπΆ)) β (β€ring RingHom
π) = {(π§ β β€ β¦ (π§(.gβπ)(1rβπ)))}) |
31 | 9, 20, 30 | 3eqtrd 2781 |
. . . . 5
β’ ((π β§ π β (BaseβπΆ)) β (β€ring(Hom
βπΆ)π) = {(π§ β β€ β¦ (π§(.gβπ)(1rβπ)))}) |
32 | | sneq 4601 |
. . . . . . 7
β’ (π = (π§ β β€ β¦ (π§(.gβπ)(1rβπ))) β {π} = {(π§ β β€ β¦ (π§(.gβπ)(1rβπ)))}) |
33 | 32 | eqeq2d 2748 |
. . . . . 6
β’ (π = (π§ β β€ β¦ (π§(.gβπ)(1rβπ))) β ((β€ring(Hom
βπΆ)π) = {π} β (β€ring(Hom
βπΆ)π) = {(π§ β β€ β¦ (π§(.gβπ)(1rβπ)))})) |
34 | 33 | spcegv 3559 |
. . . . 5
β’ ((π§ β β€ β¦ (π§(.gβπ)(1rβπ))) β V β
((β€ring(Hom βπΆ)π) = {(π§ β β€ β¦ (π§(.gβπ)(1rβπ)))} β βπ(β€ring(Hom βπΆ)π) = {π})) |
35 | 2, 31, 34 | mpsyl 68 |
. . . 4
β’ ((π β§ π β (BaseβπΆ)) β βπ(β€ring(Hom βπΆ)π) = {π}) |
36 | | eusn 4696 |
. . . 4
β’
(β!π π β
(β€ring(Hom βπΆ)π) β βπ(β€ring(Hom βπΆ)π) = {π}) |
37 | 35, 36 | sylibr 233 |
. . 3
β’ ((π β§ π β (BaseβπΆ)) β β!π π β (β€ring(Hom
βπΆ)π)) |
38 | 37 | ralrimiva 3144 |
. 2
β’ (π β βπ β (BaseβπΆ)β!π π β (β€ring(Hom
βπΆ)π)) |
39 | 3 | ringccat 46396 |
. . . 4
β’ (π β π β πΆ β Cat) |
40 | 5, 39 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
41 | 12 | a1i 11 |
. . . . 5
β’ (π β β€ring
β Ring) |
42 | 10, 41 | elind 4159 |
. . . 4
β’ (π β β€ring
β (π β©
Ring)) |
43 | 42, 16 | eleqtrrd 2841 |
. . 3
β’ (π β β€ring
β (BaseβπΆ)) |
44 | 4, 6, 40, 43 | isinito 17889 |
. 2
β’ (π β (β€ring
β (InitOβπΆ)
β βπ β
(BaseβπΆ)β!π π β (β€ring(Hom
βπΆ)π))) |
45 | 38, 44 | mpbird 257 |
1
β’ (π β β€ring
β (InitOβπΆ)) |