Step | Hyp | Ref
| Expression |
1 | | zrtermoringc.c |
. . . . . . . . . 10
β’ πΆ = (RingCatβπ) |
2 | | eqid 2737 |
. . . . . . . . . 10
β’
(BaseβπΆ) =
(BaseβπΆ) |
3 | | zrtermoringc.u |
. . . . . . . . . 10
β’ (π β π β π) |
4 | 1, 2, 3 | ringcbas 46383 |
. . . . . . . . 9
β’ (π β (BaseβπΆ) = (π β© Ring)) |
5 | 4 | eleq2d 2824 |
. . . . . . . 8
β’ (π β (π β (BaseβπΆ) β π β (π β© Ring))) |
6 | | elin 3931 |
. . . . . . . . 9
β’ (π β (π β© Ring) β (π β π β§ π β Ring)) |
7 | 6 | simprbi 498 |
. . . . . . . 8
β’ (π β (π β© Ring) β π β Ring) |
8 | 5, 7 | syl6bi 253 |
. . . . . . 7
β’ (π β (π β (BaseβπΆ) β π β Ring)) |
9 | 8 | imp 408 |
. . . . . 6
β’ ((π β§ π β (BaseβπΆ)) β π β Ring) |
10 | | zrtermoringc.z |
. . . . . . 7
β’ (π β π β (Ring β
NzRing)) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (BaseβπΆ)) β π β (Ring β
NzRing)) |
12 | | eqid 2737 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
13 | | eqid 2737 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
14 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β (Baseβπ) β¦
(0gβπ)) =
(π₯ β (Baseβπ) β¦
(0gβπ)) |
15 | 12, 13, 14 | c0rhm 46284 |
. . . . . 6
β’ ((π β Ring β§ π β (Ring β NzRing))
β (π₯ β
(Baseβπ) β¦
(0gβπ))
β (π RingHom π)) |
16 | 9, 11, 15 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β (BaseβπΆ)) β (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) |
17 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) |
18 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (BaseβπΆ)) β π β π) |
19 | | eqid 2737 |
. . . . . . . . . 10
β’ (Hom
βπΆ) = (Hom
βπΆ) |
20 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
21 | | zrtermoringc.e |
. . . . . . . . . . . . 13
β’ (π β π β π) |
22 | 10 | eldifad 3927 |
. . . . . . . . . . . . 13
β’ (π β π β Ring) |
23 | 21, 22 | elind 4159 |
. . . . . . . . . . . 12
β’ (π β π β (π β© Ring)) |
24 | 23, 4 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ (π β π β (BaseβπΆ)) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
26 | 1, 2, 18, 19, 20, 25 | ringchom 46385 |
. . . . . . . . 9
β’ ((π β§ π β (BaseβπΆ)) β (π(Hom βπΆ)π) = (π RingHom π)) |
27 | 26 | eqcomd 2743 |
. . . . . . . 8
β’ ((π β§ π β (BaseβπΆ)) β (π RingHom π) = (π(Hom βπΆ)π)) |
28 | 27 | eleq2d 2824 |
. . . . . . 7
β’ ((π β§ π β (BaseβπΆ)) β ((π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π) β (π₯ β (Baseβπ) β¦ (0gβπ)) β (π(Hom βπΆ)π))) |
29 | 28 | biimpa 478 |
. . . . . 6
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β (π₯ β (Baseβπ) β¦ (0gβπ)) β (π(Hom βπΆ)π)) |
30 | 26 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((π β§ π β (BaseβπΆ)) β (β β (π(Hom βπΆ)π) β β β (π RingHom π))) |
31 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
32 | 12, 31 | rhmf 20167 |
. . . . . . . . . 10
β’ (β β (π RingHom π) β β:(Baseβπ)βΆ(Baseβπ)) |
33 | 30, 32 | syl6bi 253 |
. . . . . . . . 9
β’ ((π β§ π β (BaseβπΆ)) β (β β (π(Hom βπΆ)π) β β:(Baseβπ)βΆ(Baseβπ))) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β (β β (π(Hom βπΆ)π) β β:(Baseβπ)βΆ(Baseβπ))) |
35 | | ffn 6673 |
. . . . . . . . . . 11
β’ (β:(Baseβπ)βΆ(Baseβπ) β β Fn (Baseβπ)) |
36 | 35 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β§ β:(Baseβπ)βΆ(Baseβπ)) β β Fn (Baseβπ)) |
37 | | fvex 6860 |
. . . . . . . . . . . 12
β’
(0gβπ) β V |
38 | 37, 14 | fnmpti 6649 |
. . . . . . . . . . 11
β’ (π₯ β (Baseβπ) β¦
(0gβπ)) Fn
(Baseβπ) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β§ β:(Baseβπ)βΆ(Baseβπ)) β (π₯ β (Baseβπ) β¦ (0gβπ)) Fn (Baseβπ)) |
40 | 31, 13 | 0ringbas 46243 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Ring β NzRing)
β (Baseβπ) =
{(0gβπ)}) |
41 | 10, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (Baseβπ) = {(0gβπ)}) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (BaseβπΆ)) β (Baseβπ) = {(0gβπ)}) |
43 | 42 | feq3d 6660 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (BaseβπΆ)) β (β:(Baseβπ)βΆ(Baseβπ) β β:(Baseβπ)βΆ{(0gβπ)})) |
44 | | fvconst 7115 |
. . . . . . . . . . . . . . 15
β’ ((β:(Baseβπ)βΆ{(0gβπ)} β§ π β (Baseβπ)) β (ββπ) = (0gβπ)) |
45 | 44 | ex 414 |
. . . . . . . . . . . . . 14
β’ (β:(Baseβπ)βΆ{(0gβπ)} β (π β (Baseβπ) β (ββπ) = (0gβπ))) |
46 | 43, 45 | syl6bi 253 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (BaseβπΆ)) β (β:(Baseβπ)βΆ(Baseβπ) β (π β (Baseβπ) β (ββπ) = (0gβπ)))) |
47 | 46 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β (β:(Baseβπ)βΆ(Baseβπ) β (π β (Baseβπ) β (ββπ) = (0gβπ)))) |
48 | 47 | imp31 419 |
. . . . . . . . . . 11
β’
(((((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β§ β:(Baseβπ)βΆ(Baseβπ)) β§ π β (Baseβπ)) β (ββπ) = (0gβπ)) |
49 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) β (π₯ β (Baseβπ) β¦ (0gβπ)) = (π₯ β (Baseβπ) β¦ (0gβπ))) |
50 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ ((π β (Baseβπ) β§ π₯ = π) β (0gβπ) = (0gβπ)) |
51 | | id 22 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) β π β (Baseβπ)) |
52 | 37 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ) β
(0gβπ)
β V) |
53 | 49, 50, 51, 52 | fvmptd 6960 |
. . . . . . . . . . . 12
β’ (π β (Baseβπ) β ((π₯ β (Baseβπ) β¦ (0gβπ))βπ) = (0gβπ)) |
54 | 53 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β§ β:(Baseβπ)βΆ(Baseβπ)) β§ π β (Baseβπ)) β ((π₯ β (Baseβπ) β¦ (0gβπ))βπ) = (0gβπ)) |
55 | 48, 54 | eqtr4d 2780 |
. . . . . . . . . 10
β’
(((((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β§ β:(Baseβπ)βΆ(Baseβπ)) β§ π β (Baseβπ)) β (ββπ) = ((π₯ β (Baseβπ) β¦ (0gβπ))βπ)) |
56 | 36, 39, 55 | eqfnfvd 6990 |
. . . . . . . . 9
β’ ((((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β§ β:(Baseβπ)βΆ(Baseβπ)) β β = (π₯ β (Baseβπ) β¦ (0gβπ))) |
57 | 56 | ex 414 |
. . . . . . . 8
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β (β:(Baseβπ)βΆ(Baseβπ) β β = (π₯ β (Baseβπ) β¦ (0gβπ)))) |
58 | 34, 57 | syld 47 |
. . . . . . 7
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β (β β (π(Hom βπΆ)π) β β = (π₯ β (Baseβπ) β¦ (0gβπ)))) |
59 | 58 | alrimiv 1931 |
. . . . . 6
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β ββ(β β (π(Hom βπΆ)π) β β = (π₯ β (Baseβπ) β¦ (0gβπ)))) |
60 | 17, 29, 59 | 3jca 1129 |
. . . . 5
β’ (((π β§ π β (BaseβπΆ)) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π)) β ((π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π(Hom βπΆ)π) β§ ββ(β β (π(Hom βπΆ)π) β β = (π₯ β (Baseβπ) β¦ (0gβπ))))) |
61 | 16, 60 | mpdan 686 |
. . . 4
β’ ((π β§ π β (BaseβπΆ)) β ((π₯ β (Baseβπ) β¦ (0gβπ)) β (π RingHom π) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π(Hom βπΆ)π) β§ ββ(β β (π(Hom βπΆ)π) β β = (π₯ β (Baseβπ) β¦ (0gβπ))))) |
62 | | eleq1 2826 |
. . . . 5
β’ (β = (π₯ β (Baseβπ) β¦ (0gβπ)) β (β β (π(Hom βπΆ)π) β (π₯ β (Baseβπ) β¦ (0gβπ)) β (π(Hom βπΆ)π))) |
63 | 62 | eqeu 3669 |
. . . 4
β’ (((π₯ β (Baseβπ) β¦
(0gβπ))
β (π RingHom π) β§ (π₯ β (Baseβπ) β¦ (0gβπ)) β (π(Hom βπΆ)π) β§ ββ(β β (π(Hom βπΆ)π) β β = (π₯ β (Baseβπ) β¦ (0gβπ)))) β β!β β β (π(Hom βπΆ)π)) |
64 | 61, 63 | syl 17 |
. . 3
β’ ((π β§ π β (BaseβπΆ)) β β!β β β (π(Hom βπΆ)π)) |
65 | 64 | ralrimiva 3144 |
. 2
β’ (π β βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π)) |
66 | 1 | ringccat 46396 |
. . . 4
β’ (π β π β πΆ β Cat) |
67 | 3, 66 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
68 | 2, 19, 67, 24 | istermo 17890 |
. 2
β’ (π β (π β (TermOβπΆ) β βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π))) |
69 | 65, 68 | mpbird 257 |
1
β’ (π β π β (TermOβπΆ)) |