Step | Hyp | Ref
| Expression |
1 | | rhmpreimacn.g |
. . . . . 6
β’ πΊ = (π β π΅ β¦ (β‘πΉ β π)) |
2 | | imaeq2 6014 |
. . . . . 6
β’ (π = π β (β‘πΉ β π) = (β‘πΉ β π)) |
3 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β π΅) β π β π΅) |
4 | | rhmpreimacn.f |
. . . . . . . . 9
β’ (π β πΉ β (π
RingHom π)) |
5 | 4 | elexd 3468 |
. . . . . . . 8
β’ (π β πΉ β V) |
6 | | cnvexg 7866 |
. . . . . . . 8
β’ (πΉ β V β β‘πΉ β V) |
7 | | imaexg 7857 |
. . . . . . . 8
β’ (β‘πΉ β V β (β‘πΉ β π) β V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . 7
β’ (π β (β‘πΉ β π) β V) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β (β‘πΉ β π) β V) |
10 | 1, 2, 3, 9 | fvmptd3 6976 |
. . . . 5
β’ ((π β§ π β π΅) β (πΊβπ) = (β‘πΉ β π)) |
11 | 10 | eleq1d 2823 |
. . . 4
β’ ((π β§ π β π΅) β ((πΊβπ) β (πβπΌ) β (β‘πΉ β π) β (πβπΌ))) |
12 | 11 | pm5.32da 580 |
. . 3
β’ (π β ((π β π΅ β§ (πΊβπ) β (πβπΌ)) β (π β π΅ β§ (β‘πΉ β π) β (πβπΌ)))) |
13 | | rhmpreimacn.s |
. . . . . . . 8
β’ (π β π β CRing) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΅) β π β CRing) |
15 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΅) β πΉ β (π
RingHom π)) |
16 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π΅) β π β π΅) |
17 | | rhmpreimacn.b |
. . . . . . . 8
β’ π΅ = (PrmIdealβπ) |
18 | 16, 17 | eleqtrdi 2848 |
. . . . . . 7
β’ ((π β§ π β π΅) β π β (PrmIdealβπ)) |
19 | | rhmpreimacn.a |
. . . . . . . 8
β’ π΄ = (PrmIdealβπ
) |
20 | 19 | rhmpreimaprmidl 32264 |
. . . . . . 7
β’ (((π β CRing β§ πΉ β (π
RingHom π)) β§ π β (PrmIdealβπ)) β (β‘πΉ β π) β π΄) |
21 | 14, 15, 18, 20 | syl21anc 837 |
. . . . . 6
β’ ((π β§ π β π΅) β (β‘πΉ β π) β π΄) |
22 | 21, 1 | fmptd 7067 |
. . . . 5
β’ (π β πΊ:π΅βΆπ΄) |
23 | 22 | ffnd 6674 |
. . . 4
β’ (π β πΊ Fn π΅) |
24 | | elpreima 7013 |
. . . 4
β’ (πΊ Fn π΅ β (π β (β‘πΊ β (πβπΌ)) β (π β π΅ β§ (πΊβπ) β (πβπΌ)))) |
25 | 23, 24 | syl 17 |
. . 3
β’ (π β (π β (β‘πΊ β (πβπΌ)) β (π β π΅ β§ (πΊβπ) β (πβπΌ)))) |
26 | | rhmpreimacnlem.w |
. . . . . . . . 9
β’ π = (π β (LIdealβπ) β¦ {π β π΅ β£ π β π}) |
27 | | sseq1 3974 |
. . . . . . . . . 10
β’ (π = (πΉ β πΌ) β (π β π β (πΉ β πΌ) β π)) |
28 | 27 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = (πΉ β πΌ) β {π β π΅ β£ π β π} = {π β π΅ β£ (πΉ β πΌ) β π}) |
29 | | rhmpreimacn.1 |
. . . . . . . . . 10
β’ (π β ran πΉ = (Baseβπ)) |
30 | | rhmpreimacnlem.1 |
. . . . . . . . . 10
β’ (π β πΌ β (LIdealβπ
)) |
31 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
32 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LIdealβπ
) =
(LIdealβπ
) |
33 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LIdealβπ) =
(LIdealβπ) |
34 | 31, 32, 33 | rhmimaidl 32246 |
. . . . . . . . . 10
β’ ((πΉ β (π
RingHom π) β§ ran πΉ = (Baseβπ) β§ πΌ β (LIdealβπ
)) β (πΉ β πΌ) β (LIdealβπ)) |
35 | 4, 29, 30, 34 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (πΉ β πΌ) β (LIdealβπ)) |
36 | 17 | fvexi 6861 |
. . . . . . . . . . 11
β’ π΅ β V |
37 | 36 | rabex 5294 |
. . . . . . . . . 10
β’ {π β π΅ β£ (πΉ β πΌ) β π} β V |
38 | 37 | a1i 11 |
. . . . . . . . 9
β’ (π β {π β π΅ β£ (πΉ β πΌ) β π} β V) |
39 | 26, 28, 35, 38 | fvmptd3 6976 |
. . . . . . . 8
β’ (π β (πβ(πΉ β πΌ)) = {π β π΅ β£ (πΉ β πΌ) β π}) |
40 | 39 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π β (πβ(πΉ β πΌ)) β π β {π β π΅ β£ (πΉ β πΌ) β π})) |
41 | | sseq2 3975 |
. . . . . . . 8
β’ (π = π β ((πΉ β πΌ) β π β (πΉ β πΌ) β π)) |
42 | 41 | elrab 3650 |
. . . . . . 7
β’ (π β {π β π΅ β£ (πΉ β πΌ) β π} β (π β π΅ β§ (πΉ β πΌ) β π)) |
43 | 40, 42 | bitrdi 287 |
. . . . . 6
β’ (π β (π β (πβ(πΉ β πΌ)) β (π β π΅ β§ (πΉ β πΌ) β π))) |
44 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
45 | 44, 31 | rhmf 20167 |
. . . . . . . . . 10
β’ (πΉ β (π
RingHom π) β πΉ:(Baseβπ
)βΆ(Baseβπ)) |
46 | 4, 45 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ:(Baseβπ
)βΆ(Baseβπ)) |
47 | 46 | ffund 6677 |
. . . . . . . 8
β’ (π β Fun πΉ) |
48 | 44, 32 | lidlss 20696 |
. . . . . . . . . 10
β’ (πΌ β (LIdealβπ
) β πΌ β (Baseβπ
)) |
49 | 30, 48 | syl 17 |
. . . . . . . . 9
β’ (π β πΌ β (Baseβπ
)) |
50 | 46 | fdmd 6684 |
. . . . . . . . 9
β’ (π β dom πΉ = (Baseβπ
)) |
51 | 49, 50 | sseqtrrd 3990 |
. . . . . . . 8
β’ (π β πΌ β dom πΉ) |
52 | | funimass3 7009 |
. . . . . . . 8
β’ ((Fun
πΉ β§ πΌ β dom πΉ) β ((πΉ β πΌ) β π β πΌ β (β‘πΉ β π))) |
53 | 47, 51, 52 | syl2anc 585 |
. . . . . . 7
β’ (π β ((πΉ β πΌ) β π β πΌ β (β‘πΉ β π))) |
54 | 53 | anbi2d 630 |
. . . . . 6
β’ (π β ((π β π΅ β§ (πΉ β πΌ) β π) β (π β π΅ β§ πΌ β (β‘πΉ β π)))) |
55 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β CRing) |
56 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β πΉ β (π
RingHom π)) |
57 | 3, 17 | eleqtrdi 2848 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β (PrmIdealβπ)) |
58 | 19 | rhmpreimaprmidl 32264 |
. . . . . . . . 9
β’ (((π β CRing β§ πΉ β (π
RingHom π)) β§ π β (PrmIdealβπ)) β (β‘πΉ β π) β π΄) |
59 | 55, 56, 57, 58 | syl21anc 837 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (β‘πΉ β π) β π΄) |
60 | 59 | biantrurd 534 |
. . . . . . 7
β’ ((π β§ π β π΅) β (πΌ β (β‘πΉ β π) β ((β‘πΉ β π) β π΄ β§ πΌ β (β‘πΉ β π)))) |
61 | 60 | pm5.32da 580 |
. . . . . 6
β’ (π β ((π β π΅ β§ πΌ β (β‘πΉ β π)) β (π β π΅ β§ ((β‘πΉ β π) β π΄ β§ πΌ β (β‘πΉ β π))))) |
62 | 43, 54, 61 | 3bitrd 305 |
. . . . 5
β’ (π β (π β (πβ(πΉ β πΌ)) β (π β π΅ β§ ((β‘πΉ β π) β π΄ β§ πΌ β (β‘πΉ β π))))) |
63 | | sseq2 3975 |
. . . . . . 7
β’ (π = (β‘πΉ β π) β (πΌ β π β πΌ β (β‘πΉ β π))) |
64 | 63 | elrab 3650 |
. . . . . 6
β’ ((β‘πΉ β π) β {π β π΄ β£ πΌ β π} β ((β‘πΉ β π) β π΄ β§ πΌ β (β‘πΉ β π))) |
65 | 64 | anbi2i 624 |
. . . . 5
β’ ((π β π΅ β§ (β‘πΉ β π) β {π β π΄ β£ πΌ β π}) β (π β π΅ β§ ((β‘πΉ β π) β π΄ β§ πΌ β (β‘πΉ β π)))) |
66 | 62, 65 | bitr4di 289 |
. . . 4
β’ (π β (π β (πβ(πΉ β πΌ)) β (π β π΅ β§ (β‘πΉ β π) β {π β π΄ β£ πΌ β π}))) |
67 | | rhmpreimacnlem.v |
. . . . . . 7
β’ π = (π β (LIdealβπ
) β¦ {π β π΄ β£ π β π}) |
68 | | sseq1 3974 |
. . . . . . . 8
β’ (π = πΌ β (π β π β πΌ β π)) |
69 | 68 | rabbidv 3418 |
. . . . . . 7
β’ (π = πΌ β {π β π΄ β£ π β π} = {π β π΄ β£ πΌ β π}) |
70 | 19 | fvexi 6861 |
. . . . . . . . 9
β’ π΄ β V |
71 | 70 | rabex 5294 |
. . . . . . . 8
β’ {π β π΄ β£ πΌ β π} β V |
72 | 71 | a1i 11 |
. . . . . . 7
β’ (π β {π β π΄ β£ πΌ β π} β V) |
73 | 67, 69, 30, 72 | fvmptd3 6976 |
. . . . . 6
β’ (π β (πβπΌ) = {π β π΄ β£ πΌ β π}) |
74 | 73 | eleq2d 2824 |
. . . . 5
β’ (π β ((β‘πΉ β π) β (πβπΌ) β (β‘πΉ β π) β {π β π΄ β£ πΌ β π})) |
75 | 74 | anbi2d 630 |
. . . 4
β’ (π β ((π β π΅ β§ (β‘πΉ β π) β (πβπΌ)) β (π β π΅ β§ (β‘πΉ β π) β {π β π΄ β£ πΌ β π}))) |
76 | 66, 75 | bitr4d 282 |
. . 3
β’ (π β (π β (πβ(πΉ β πΌ)) β (π β π΅ β§ (β‘πΉ β π) β (πβπΌ)))) |
77 | 12, 25, 76 | 3bitr4rd 312 |
. 2
β’ (π β (π β (πβ(πΉ β πΌ)) β π β (β‘πΊ β (πβπΌ)))) |
78 | 77 | eqrdv 2735 |
1
β’ (π β (πβ(πΉ β πΌ)) = (β‘πΊ β (πβπΌ))) |