Step | Hyp | Ref
| Expression |
1 | | qusrhm.x |
. 2
β’ π = (Baseβπ
) |
2 | | eqid 2733 |
. 2
β’
(1rβπ
) = (1rβπ
) |
3 | | eqid 2733 |
. 2
β’
(1rβπ) = (1rβπ) |
4 | | eqid 2733 |
. 2
β’
(.rβπ
) = (.rβπ
) |
5 | | eqid 2733 |
. 2
β’
(.rβπ) = (.rβπ) |
6 | | simpl 484 |
. 2
β’ ((π
β Ring β§ π β πΌ) β π
β Ring) |
7 | | qusring.u |
. . 3
β’ π = (π
/s (π
~QG π)) |
8 | | qusring.i |
. . 3
β’ πΌ = (2Idealβπ
) |
9 | 7, 8 | qusring 20722 |
. 2
β’ ((π
β Ring β§ π β πΌ) β π β Ring) |
10 | | eqid 2733 |
. . . . . . . . 9
β’
(LIdealβπ
) =
(LIdealβπ
) |
11 | | eqid 2733 |
. . . . . . . . 9
β’
(opprβπ
) = (opprβπ
) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(LIdealβ(opprβπ
)) =
(LIdealβ(opprβπ
)) |
13 | 10, 11, 12, 8 | 2idlval 20719 |
. . . . . . . 8
β’ πΌ = ((LIdealβπ
) β©
(LIdealβ(opprβπ
))) |
14 | 13 | elin2 4158 |
. . . . . . 7
β’ (π β πΌ β (π β (LIdealβπ
) β§ π β
(LIdealβ(opprβπ
)))) |
15 | 14 | simplbi 499 |
. . . . . 6
β’ (π β πΌ β π β (LIdealβπ
)) |
16 | 10 | lidlsubg 20701 |
. . . . . 6
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (SubGrpβπ
)) |
17 | 15, 16 | sylan2 594 |
. . . . 5
β’ ((π
β Ring β§ π β πΌ) β π β (SubGrpβπ
)) |
18 | | eqid 2733 |
. . . . . 6
β’ (π
~QG π) = (π
~QG π) |
19 | 1, 18 | eqger 18985 |
. . . . 5
β’ (π β (SubGrpβπ
) β (π
~QG π) Er π) |
20 | 17, 19 | syl 17 |
. . . 4
β’ ((π
β Ring β§ π β πΌ) β (π
~QG π) Er π) |
21 | 1 | fvexi 6857 |
. . . . 5
β’ π β V |
22 | 21 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ π β πΌ) β π β V) |
23 | | qusrhm.f |
. . . 4
β’ πΉ = (π₯ β π β¦ [π₯](π
~QG π)) |
24 | 20, 22, 23 | divsfval 17434 |
. . 3
β’ ((π
β Ring β§ π β πΌ) β (πΉβ(1rβπ
)) = [(1rβπ
)](π
~QG π)) |
25 | 7, 8, 2 | qus1 20721 |
. . . 4
β’ ((π
β Ring β§ π β πΌ) β (π β Ring β§
[(1rβπ
)](π
~QG π) = (1rβπ))) |
26 | 25 | simprd 497 |
. . 3
β’ ((π
β Ring β§ π β πΌ) β [(1rβπ
)](π
~QG π) = (1rβπ)) |
27 | 24, 26 | eqtrd 2773 |
. 2
β’ ((π
β Ring β§ π β πΌ) β (πΉβ(1rβπ
)) = (1rβπ)) |
28 | 7 | a1i 11 |
. . . . 5
β’ ((π
β Ring β§ π β πΌ) β π = (π
/s (π
~QG π))) |
29 | 1 | a1i 11 |
. . . . 5
β’ ((π
β Ring β§ π β πΌ) β π = (Baseβπ
)) |
30 | 1, 18, 8, 4 | 2idlcpbl 20720 |
. . . . 5
β’ ((π
β Ring β§ π β πΌ) β ((π(π
~QG π)π β§ π(π
~QG π)π) β (π(.rβπ
)π)(π
~QG π)(π(.rβπ
)π))) |
31 | 1, 4 | ringcl 19986 |
. . . . . . . 8
β’ ((π
β Ring β§ π¦ β π β§ π§ β π) β (π¦(.rβπ
)π§) β π) |
32 | 31 | 3expb 1121 |
. . . . . . 7
β’ ((π
β Ring β§ (π¦ β π β§ π§ β π)) β (π¦(.rβπ
)π§) β π) |
33 | 32 | adantlr 714 |
. . . . . 6
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β (π¦(.rβπ
)π§) β π) |
34 | 33 | caovclg 7547 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π β π β§ π β π)) β (π(.rβπ
)π) β π) |
35 | 28, 29, 20, 6, 30, 34, 4, 5 | qusmulval 17442 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ π¦ β π β§ π§ β π) β ([π¦](π
~QG π)(.rβπ)[π§](π
~QG π)) = [(π¦(.rβπ
)π§)](π
~QG π)) |
36 | 35 | 3expb 1121 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β ([π¦](π
~QG π)(.rβπ)[π§](π
~QG π)) = [(π¦(.rβπ
)π§)](π
~QG π)) |
37 | 20 | adantr 482 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β (π
~QG π) Er π) |
38 | 21 | a1i 11 |
. . . . 5
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β π β V) |
39 | 37, 38, 23 | divsfval 17434 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β (πΉβπ¦) = [π¦](π
~QG π)) |
40 | 37, 38, 23 | divsfval 17434 |
. . . 4
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β (πΉβπ§) = [π§](π
~QG π)) |
41 | 39, 40 | oveq12d 7376 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β ((πΉβπ¦)(.rβπ)(πΉβπ§)) = ([π¦](π
~QG π)(.rβπ)[π§](π
~QG π))) |
42 | 37, 38, 23 | divsfval 17434 |
. . 3
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β (πΉβ(π¦(.rβπ
)π§)) = [(π¦(.rβπ
)π§)](π
~QG π)) |
43 | 36, 41, 42 | 3eqtr4rd 2784 |
. 2
β’ (((π
β Ring β§ π β πΌ) β§ (π¦ β π β§ π§ β π)) β (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦)(.rβπ)(πΉβπ§))) |
44 | | ringabl 20007 |
. . . . . 6
β’ (π
β Ring β π
β Abel) |
45 | 44 | adantr 482 |
. . . . 5
β’ ((π
β Ring β§ π β πΌ) β π
β Abel) |
46 | | ablnsg 19630 |
. . . . 5
β’ (π
β Abel β
(NrmSGrpβπ
) =
(SubGrpβπ
)) |
47 | 45, 46 | syl 17 |
. . . 4
β’ ((π
β Ring β§ π β πΌ) β (NrmSGrpβπ
) = (SubGrpβπ
)) |
48 | 17, 47 | eleqtrrd 2837 |
. . 3
β’ ((π
β Ring β§ π β πΌ) β π β (NrmSGrpβπ
)) |
49 | 1, 7, 23 | qusghm 19050 |
. . 3
β’ (π β (NrmSGrpβπ
) β πΉ β (π
GrpHom π)) |
50 | 48, 49 | syl 17 |
. 2
β’ ((π
β Ring β§ π β πΌ) β πΉ β (π
GrpHom π)) |
51 | 1, 2, 3, 4, 5, 6, 9, 27, 43, 50 | isrhm2d 20167 |
1
β’ ((π
β Ring β§ π β πΌ) β πΉ β (π
RingHom π)) |