Step | Hyp | Ref
| Expression |
1 | | eqid 2727 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2727 |
. 2
β’
(1rβπ) = (1rβπ) |
3 | | eqid 2727 |
. 2
β’
(1rβπ») = (1rβπ») |
4 | | eqid 2727 |
. 2
β’
(.rβπ) = (.rβπ) |
5 | | eqid 2727 |
. 2
β’
(.rβπ») = (.rβπ») |
6 | | rhmqusker.f |
. . . . 5
β’ (π β πΉ β (πΊ RingHom π»)) |
7 | | rhmrcl1 20397 |
. . . . 5
β’ (πΉ β (πΊ RingHom π») β πΊ β Ring) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β πΊ β Ring) |
9 | | rhmqusker.k |
. . . . . 6
β’ πΎ = (β‘πΉ β { 0 }) |
10 | | eqid 2727 |
. . . . . . . 8
β’
(LIdealβπΊ) =
(LIdealβπΊ) |
11 | | rhmqusker.1 |
. . . . . . . 8
β’ 0 =
(0gβπ») |
12 | 10, 11 | kerlidl 33058 |
. . . . . . 7
β’ (πΉ β (πΊ RingHom π») β (β‘πΉ β { 0 }) β
(LIdealβπΊ)) |
13 | 6, 12 | syl 17 |
. . . . . 6
β’ (π β (β‘πΉ β { 0 }) β
(LIdealβπΊ)) |
14 | 9, 13 | eqeltrid 2832 |
. . . . 5
β’ (π β πΎ β (LIdealβπΊ)) |
15 | | rhmquskerlem.2 |
. . . . . 6
β’ (π β πΊ β CRing) |
16 | 10 | crng2idl 21155 |
. . . . . 6
β’ (πΊ β CRing β
(LIdealβπΊ) =
(2IdealβπΊ)) |
17 | 15, 16 | syl 17 |
. . . . 5
β’ (π β (LIdealβπΊ) = (2IdealβπΊ)) |
18 | 14, 17 | eleqtrd 2830 |
. . . 4
β’ (π β πΎ β (2IdealβπΊ)) |
19 | | rhmqusker.q |
. . . . 5
β’ π = (πΊ /s (πΊ ~QG πΎ)) |
20 | | eqid 2727 |
. . . . 5
β’
(2IdealβπΊ) =
(2IdealβπΊ) |
21 | | eqid 2727 |
. . . . 5
β’
(1rβπΊ) = (1rβπΊ) |
22 | 19, 20, 21 | qus1 21150 |
. . . 4
β’ ((πΊ β Ring β§ πΎ β (2IdealβπΊ)) β (π β Ring β§
[(1rβπΊ)](πΊ ~QG πΎ) = (1rβπ))) |
23 | 8, 18, 22 | syl2anc 583 |
. . 3
β’ (π β (π β Ring β§
[(1rβπΊ)](πΊ ~QG πΎ) = (1rβπ))) |
24 | 23 | simpld 494 |
. 2
β’ (π β π β Ring) |
25 | | rhmrcl2 20398 |
. . 3
β’ (πΉ β (πΊ RingHom π») β π» β Ring) |
26 | 6, 25 | syl 17 |
. 2
β’ (π β π» β Ring) |
27 | | rhmghm 20405 |
. . . . 5
β’ (πΉ β (πΊ RingHom π») β πΉ β (πΊ GrpHom π»)) |
28 | 6, 27 | syl 17 |
. . . 4
β’ (π β πΉ β (πΊ GrpHom π»)) |
29 | | rhmquskerlem.j |
. . . 4
β’ π½ = (π β (Baseβπ) β¦ βͺ
(πΉ β π)) |
30 | | eqid 2727 |
. . . . . 6
β’
(BaseβπΊ) =
(BaseβπΊ) |
31 | 30, 21 | ringidcl 20184 |
. . . . 5
β’ (πΊ β Ring β
(1rβπΊ)
β (BaseβπΊ)) |
32 | 8, 31 | syl 17 |
. . . 4
β’ (π β (1rβπΊ) β (BaseβπΊ)) |
33 | 11, 28, 9, 19, 29, 32 | ghmquskerlem1 19218 |
. . 3
β’ (π β (π½β[(1rβπΊ)](πΊ ~QG πΎ)) = (πΉβ(1rβπΊ))) |
34 | 23 | simprd 495 |
. . . 4
β’ (π β
[(1rβπΊ)](πΊ ~QG πΎ) = (1rβπ)) |
35 | 34 | fveq2d 6895 |
. . 3
β’ (π β (π½β[(1rβπΊ)](πΊ ~QG πΎ)) = (π½β(1rβπ))) |
36 | 21, 3 | rhm1 20410 |
. . . 4
β’ (πΉ β (πΊ RingHom π») β (πΉβ(1rβπΊ)) = (1rβπ»)) |
37 | 6, 36 | syl 17 |
. . 3
β’ (π β (πΉβ(1rβπΊ)) = (1rβπ»)) |
38 | 33, 35, 37 | 3eqtr3d 2775 |
. 2
β’ (π β (π½β(1rβπ)) = (1rβπ»)) |
39 | 6 | ad6antr 735 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β πΉ β (πΊ RingHom π»)) |
40 | 19 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π = (πΊ /s (πΊ ~QG πΎ))) |
41 | | eqidd 2728 |
. . . . . . . . . . . . 13
β’ (π β (BaseβπΊ) = (BaseβπΊ)) |
42 | | ovexd 7449 |
. . . . . . . . . . . . 13
β’ (π β (πΊ ~QG πΎ) β V) |
43 | 40, 41, 42, 15 | qusbas 17512 |
. . . . . . . . . . . 12
β’ (π β ((BaseβπΊ) / (πΊ ~QG πΎ)) = (Baseβπ)) |
44 | 11 | ghmker 19180 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (πΊ GrpHom π») β (β‘πΉ β { 0 }) β
(NrmSGrpβπΊ)) |
45 | 28, 44 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (β‘πΉ β { 0 }) β
(NrmSGrpβπΊ)) |
46 | 9, 45 | eqeltrid 2832 |
. . . . . . . . . . . . . 14
β’ (π β πΎ β (NrmSGrpβπΊ)) |
47 | | nsgsubg 19097 |
. . . . . . . . . . . . . 14
β’ (πΎ β (NrmSGrpβπΊ) β πΎ β (SubGrpβπΊ)) |
48 | | eqid 2727 |
. . . . . . . . . . . . . . 15
β’ (πΊ ~QG πΎ) = (πΊ ~QG πΎ) |
49 | 30, 48 | eqger 19117 |
. . . . . . . . . . . . . 14
β’ (πΎ β (SubGrpβπΊ) β (πΊ ~QG πΎ) Er (BaseβπΊ)) |
50 | 46, 47, 49 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β (πΊ ~QG πΎ) Er (BaseβπΊ)) |
51 | 50 | qsss 8786 |
. . . . . . . . . . . 12
β’ (π β ((BaseβπΊ) / (πΊ ~QG πΎ)) β π« (BaseβπΊ)) |
52 | 43, 51 | eqsstrrd 4017 |
. . . . . . . . . . 11
β’ (π β (Baseβπ) β π«
(BaseβπΊ)) |
53 | 52 | sselda 3978 |
. . . . . . . . . 10
β’ ((π β§ π β (Baseβπ)) β π β π« (BaseβπΊ)) |
54 | 53 | elpwid 4607 |
. . . . . . . . 9
β’ ((π β§ π β (Baseβπ)) β π β (BaseβπΊ)) |
55 | 54 | ad5antr 733 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π β (BaseβπΊ)) |
56 | | simp-4r 783 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π₯ β π) |
57 | 55, 56 | sseldd 3979 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π₯ β (BaseβπΊ)) |
58 | 52 | sselda 3978 |
. . . . . . . . . . 11
β’ ((π β§ π β (Baseβπ)) β π β π« (BaseβπΊ)) |
59 | 58 | elpwid 4607 |
. . . . . . . . . 10
β’ ((π β§ π β (Baseβπ)) β π β (BaseβπΊ)) |
60 | 59 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β π β (BaseβπΊ)) |
61 | 60 | ad4antr 731 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π β (BaseβπΊ)) |
62 | | simplr 768 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π¦ β π ) |
63 | 61, 62 | sseldd 3979 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π¦ β (BaseβπΊ)) |
64 | | eqid 2727 |
. . . . . . . 8
β’
(.rβπΊ) = (.rβπΊ) |
65 | 30, 64, 5 | rhmmul 20407 |
. . . . . . 7
β’ ((πΉ β (πΊ RingHom π») β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β (πΉβ(π₯(.rβπΊ)π¦)) = ((πΉβπ₯)(.rβπ»)(πΉβπ¦))) |
66 | 39, 57, 63, 65 | syl3anc 1369 |
. . . . . 6
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (πΉβ(π₯(.rβπΊ)π¦)) = ((πΉβπ₯)(.rβπ»)(πΉβπ¦))) |
67 | 50 | ad6antr 735 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (πΊ ~QG πΎ) Er (BaseβπΊ)) |
68 | | simp-6r 787 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π β (Baseβπ)) |
69 | 43 | ad6antr 735 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β ((BaseβπΊ) / (πΊ ~QG πΎ)) = (Baseβπ)) |
70 | 68, 69 | eleqtrrd 2831 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π β ((BaseβπΊ) / (πΊ ~QG πΎ))) |
71 | | qsel 8804 |
. . . . . . . . . . 11
β’ (((πΊ ~QG πΎ) Er (BaseβπΊ) β§ π β ((BaseβπΊ) / (πΊ ~QG πΎ)) β§ π₯ β π) β π = [π₯](πΊ ~QG πΎ)) |
72 | 67, 70, 56, 71 | syl3anc 1369 |
. . . . . . . . . 10
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π = [π₯](πΊ ~QG πΎ)) |
73 | | simp-5r 785 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π β (Baseβπ)) |
74 | 73, 69 | eleqtrrd 2831 |
. . . . . . . . . . 11
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π β ((BaseβπΊ) / (πΊ ~QG πΎ))) |
75 | | qsel 8804 |
. . . . . . . . . . 11
β’ (((πΊ ~QG πΎ) Er (BaseβπΊ) β§ π β ((BaseβπΊ) / (πΊ ~QG πΎ)) β§ π¦ β π ) β π = [π¦](πΊ ~QG πΎ)) |
76 | 67, 74, 62, 75 | syl3anc 1369 |
. . . . . . . . . 10
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β π = [π¦](πΊ ~QG πΎ)) |
77 | 72, 76 | oveq12d 7432 |
. . . . . . . . 9
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π(.rβπ)π ) = ([π₯](πΊ ~QG πΎ)(.rβπ)[π¦](πΊ ~QG πΎ))) |
78 | 15 | ad6antr 735 |
. . . . . . . . . 10
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β πΊ β CRing) |
79 | 14 | ad6antr 735 |
. . . . . . . . . 10
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β πΎ β (LIdealβπΊ)) |
80 | 19, 30, 64, 4, 78, 79, 57, 63 | qusmul 33041 |
. . . . . . . . 9
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β ([π₯](πΊ ~QG πΎ)(.rβπ)[π¦](πΊ ~QG πΎ)) = [(π₯(.rβπΊ)π¦)](πΊ ~QG πΎ)) |
81 | 77, 80 | eqtr2d 2768 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β [(π₯(.rβπΊ)π¦)](πΊ ~QG πΎ) = (π(.rβπ)π )) |
82 | 81 | fveq2d 6895 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π½β[(π₯(.rβπΊ)π¦)](πΊ ~QG πΎ)) = (π½β(π(.rβπ)π ))) |
83 | 39, 27 | syl 17 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β πΉ β (πΊ GrpHom π»)) |
84 | 39, 7 | syl 17 |
. . . . . . . . 9
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β πΊ β Ring) |
85 | 30, 64, 84, 57, 63 | ringcld 20181 |
. . . . . . . 8
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π₯(.rβπΊ)π¦) β (BaseβπΊ)) |
86 | 11, 83, 9, 19, 29, 85 | ghmquskerlem1 19218 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π½β[(π₯(.rβπΊ)π¦)](πΊ ~QG πΎ)) = (πΉβ(π₯(.rβπΊ)π¦))) |
87 | 82, 86 | eqtr3d 2769 |
. . . . . 6
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π½β(π(.rβπ)π )) = (πΉβ(π₯(.rβπΊ)π¦))) |
88 | | simpllr 775 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π½βπ) = (πΉβπ₯)) |
89 | | simpr 484 |
. . . . . . 7
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π½βπ ) = (πΉβπ¦)) |
90 | 88, 89 | oveq12d 7432 |
. . . . . 6
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β ((π½βπ)(.rβπ»)(π½βπ )) = ((πΉβπ₯)(.rβπ»)(πΉβπ¦))) |
91 | 66, 87, 90 | 3eqtr4d 2777 |
. . . . 5
β’
(((((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β§ π¦ β π ) β§ (π½βπ ) = (πΉβπ¦)) β (π½β(π(.rβπ)π )) = ((π½βπ)(.rβπ»)(π½βπ ))) |
92 | 28 | ad4antr 731 |
. . . . . 6
β’
(((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β πΉ β (πΊ GrpHom π»)) |
93 | | simpllr 775 |
. . . . . 6
β’
(((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β π β (Baseβπ)) |
94 | 11, 92, 9, 19, 29, 93 | ghmquskerlem2 19220 |
. . . . 5
β’
(((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β βπ¦ β π (π½βπ ) = (πΉβπ¦)) |
95 | 91, 94 | r19.29a 3157 |
. . . 4
β’
(((((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β§ π₯ β π) β§ (π½βπ) = (πΉβπ₯)) β (π½β(π(.rβπ)π )) = ((π½βπ)(.rβπ»)(π½βπ ))) |
96 | 28 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β πΉ β (πΊ GrpHom π»)) |
97 | | simplr 768 |
. . . . 5
β’ (((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β π β (Baseβπ)) |
98 | 11, 96, 9, 19, 29, 97 | ghmquskerlem2 19220 |
. . . 4
β’ (((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β βπ₯ β π (π½βπ) = (πΉβπ₯)) |
99 | 95, 98 | r19.29a 3157 |
. . 3
β’ (((π β§ π β (Baseβπ)) β§ π β (Baseβπ)) β (π½β(π(.rβπ)π )) = ((π½βπ)(.rβπ»)(π½βπ ))) |
100 | 99 | anasss 466 |
. 2
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β (π½β(π(.rβπ)π )) = ((π½βπ)(.rβπ»)(π½βπ ))) |
101 | 11, 28, 9, 19, 29 | ghmquskerlem3 19221 |
. 2
β’ (π β π½ β (π GrpHom π»)) |
102 | 1, 2, 3, 4, 5, 24,
26, 38, 100, 101 | isrhm2d 20408 |
1
β’ (π β π½ β (π RingHom π»)) |