Step | Hyp | Ref
| Expression |
1 | | brric 20406 |
. . 3
β’ (π
βπ
π β (π
RingIso π) β β
) |
2 | | n0 4341 |
. . 3
β’ ((π
RingIso π) β β
β βπ π β (π
RingIso π)) |
3 | 1, 2 | bitri 275 |
. 2
β’ (π
βπ
π β βπ π β (π
RingIso π)) |
4 | | eqid 2726 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
5 | | eqid 2726 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
6 | 4, 5 | rimf1o 20396 |
. . . . . . . . . 10
β’ (π β (π
RingIso π) β π:(Baseβπ
)β1-1-ontoβ(Baseβπ)) |
7 | | f1ofo 6834 |
. . . . . . . . . 10
β’ (π:(Baseβπ
)β1-1-ontoβ(Baseβπ) β π:(Baseβπ
)βontoβ(Baseβπ)) |
8 | | foima 6804 |
. . . . . . . . . 10
β’ (π:(Baseβπ
)βontoβ(Baseβπ) β (π β (Baseβπ
)) = (Baseβπ)) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . 9
β’ (π β (π
RingIso π) β (π β (Baseβπ
)) = (Baseβπ)) |
10 | 9 | oveq2d 7421 |
. . . . . . . 8
β’ (π β (π
RingIso π) β (π βΎs (π β (Baseβπ
))) = (π βΎs (Baseβπ))) |
11 | | rimrcl2 41650 |
. . . . . . . . 9
β’ (π β (π
RingIso π) β π β Ring) |
12 | 5 | ressid 17198 |
. . . . . . . . 9
β’ (π β Ring β (π βΎs
(Baseβπ)) = π) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ (π β (π
RingIso π) β (π βΎs (Baseβπ)) = π) |
14 | 10, 13 | eqtr2d 2767 |
. . . . . . 7
β’ (π β (π
RingIso π) β π = (π βΎs (π β (Baseβπ
)))) |
15 | 14 | adantr 480 |
. . . . . 6
β’ ((π β (π
RingIso π) β§ π
β DivRing) β π = (π βΎs (π β (Baseβπ
)))) |
16 | | eqid 2726 |
. . . . . . 7
β’ (π βΎs (π β (Baseβπ
))) = (π βΎs (π β (Baseβπ
))) |
17 | | eqid 2726 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
18 | | rimrhm 20398 |
. . . . . . . 8
β’ (π β (π
RingIso π) β π β (π
RingHom π)) |
19 | 18 | adantr 480 |
. . . . . . 7
β’ ((π β (π
RingIso π) β§ π
β DivRing) β π β (π
RingHom π)) |
20 | 4 | sdrgid 20643 |
. . . . . . . 8
β’ (π
β DivRing β
(Baseβπ
) β
(SubDRingβπ
)) |
21 | 20 | adantl 481 |
. . . . . . 7
β’ ((π β (π
RingIso π) β§ π
β DivRing) β (Baseβπ
) β (SubDRingβπ
)) |
22 | | forn 6802 |
. . . . . . . . . 10
β’ (π:(Baseβπ
)βontoβ(Baseβπ) β ran π = (Baseβπ)) |
23 | 6, 7, 22 | 3syl 18 |
. . . . . . . . 9
β’ (π β (π
RingIso π) β ran π = (Baseβπ)) |
24 | 23 | adantr 480 |
. . . . . . . 8
β’ ((π β (π
RingIso π) β§ π
β DivRing) β ran π = (Baseβπ)) |
25 | | rhmrcl2 20379 |
. . . . . . . . . 10
β’ (π β (π
RingHom π) β π β Ring) |
26 | | eqid 2726 |
. . . . . . . . . . 11
β’
(1rβπ) = (1rβπ) |
27 | 5, 26 | ringidcl 20165 |
. . . . . . . . . 10
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
28 | 18, 25, 27 | 3syl 18 |
. . . . . . . . 9
β’ (π β (π
RingIso π) β (1rβπ) β (Baseβπ)) |
29 | | eqid 2726 |
. . . . . . . . . . . . . 14
β’
(0gβπ
) = (0gβπ
) |
30 | | eqid 2726 |
. . . . . . . . . . . . . 14
β’
(1rβπ
) = (1rβπ
) |
31 | 29, 30 | drngunz 20606 |
. . . . . . . . . . . . 13
β’ (π
β DivRing β
(1rβπ
)
β (0gβπ
)) |
32 | 31 | adantl 481 |
. . . . . . . . . . . 12
β’ ((π β (π
RingIso π) β§ π
β DivRing) β
(1rβπ
)
β (0gβπ
)) |
33 | | f1of1 6826 |
. . . . . . . . . . . . . . 15
β’ (π:(Baseβπ
)β1-1-ontoβ(Baseβπ) β π:(Baseβπ
)β1-1β(Baseβπ)) |
34 | 6, 33 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π
RingIso π) β π:(Baseβπ
)β1-1β(Baseβπ)) |
35 | | drngring 20594 |
. . . . . . . . . . . . . . . 16
β’ (π
β DivRing β π
β Ring) |
36 | 4, 30 | ringidcl 20165 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π
β DivRing β
(1rβπ
)
β (Baseβπ
)) |
38 | 4, 29 | ring0cl 20166 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β
(0gβπ
)
β (Baseβπ
)) |
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π
β DivRing β
(0gβπ
)
β (Baseβπ
)) |
40 | 37, 39 | jca 511 |
. . . . . . . . . . . . . 14
β’ (π
β DivRing β
((1rβπ
)
β (Baseβπ
) β§
(0gβπ
)
β (Baseβπ
))) |
41 | | f1veqaeq 7252 |
. . . . . . . . . . . . . 14
β’ ((π:(Baseβπ
)β1-1β(Baseβπ) β§ ((1rβπ
) β (Baseβπ
) β§
(0gβπ
)
β (Baseβπ
)))
β ((πβ(1rβπ
)) = (πβ(0gβπ
)) β (1rβπ
) = (0gβπ
))) |
42 | 34, 40, 41 | syl2an 595 |
. . . . . . . . . . . . 13
β’ ((π β (π
RingIso π) β§ π
β DivRing) β ((πβ(1rβπ
)) = (πβ(0gβπ
)) β (1rβπ
) = (0gβπ
))) |
43 | 42 | imp 406 |
. . . . . . . . . . . 12
β’ (((π β (π
RingIso π) β§ π
β DivRing) β§ (πβ(1rβπ
)) = (πβ(0gβπ
))) β (1rβπ
) = (0gβπ
)) |
44 | 32, 43 | mteqand 3027 |
. . . . . . . . . . 11
β’ ((π β (π
RingIso π) β§ π
β DivRing) β (πβ(1rβπ
)) β (πβ(0gβπ
))) |
45 | 30, 26 | rhm1 20391 |
. . . . . . . . . . . 12
β’ (π β (π
RingHom π) β (πβ(1rβπ
)) = (1rβπ)) |
46 | 19, 45 | syl 17 |
. . . . . . . . . . 11
β’ ((π β (π
RingIso π) β§ π
β DivRing) β (πβ(1rβπ
)) = (1rβπ)) |
47 | | rhmghm 20386 |
. . . . . . . . . . . 12
β’ (π β (π
RingHom π) β π β (π
GrpHom π)) |
48 | 29, 17 | ghmid 19147 |
. . . . . . . . . . . 12
β’ (π β (π
GrpHom π) β (πβ(0gβπ
)) = (0gβπ)) |
49 | 19, 47, 48 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β (π
RingIso π) β§ π
β DivRing) β (πβ(0gβπ
)) = (0gβπ)) |
50 | 44, 46, 49 | 3netr3d 3011 |
. . . . . . . . . 10
β’ ((π β (π
RingIso π) β§ π
β DivRing) β
(1rβπ)
β (0gβπ)) |
51 | | nelsn 4663 |
. . . . . . . . . 10
β’
((1rβπ) β (0gβπ) β Β¬
(1rβπ)
β {(0gβπ)}) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
β’ ((π β (π
RingIso π) β§ π
β DivRing) β Β¬
(1rβπ)
β {(0gβπ)}) |
53 | | nelne1 3033 |
. . . . . . . . 9
β’
(((1rβπ) β (Baseβπ) β§ Β¬ (1rβπ) β
{(0gβπ)})
β (Baseβπ) β
{(0gβπ)}) |
54 | 28, 52, 53 | syl2an2r 682 |
. . . . . . . 8
β’ ((π β (π
RingIso π) β§ π
β DivRing) β (Baseβπ) β
{(0gβπ)}) |
55 | 24, 54 | eqnetrd 3002 |
. . . . . . 7
β’ ((π β (π
RingIso π) β§ π
β DivRing) β ran π β
{(0gβπ)}) |
56 | 16, 17, 19, 21, 55 | imadrhmcl 20648 |
. . . . . 6
β’ ((π β (π
RingIso π) β§ π
β DivRing) β (π βΎs (π β (Baseβπ
))) β DivRing) |
57 | 15, 56 | eqeltrd 2827 |
. . . . 5
β’ ((π β (π
RingIso π) β§ π
β DivRing) β π β DivRing) |
58 | 57 | ex 412 |
. . . 4
β’ (π β (π
RingIso π) β (π
β DivRing β π β DivRing)) |
59 | 58 | exlimiv 1925 |
. . 3
β’
(βπ π β (π
RingIso π) β (π
β DivRing β π β DivRing)) |
60 | 59 | imp 406 |
. 2
β’
((βπ π β (π
RingIso π) β§ π
β DivRing) β π β DivRing) |
61 | 3, 60 | sylanb 580 |
1
β’ ((π
βπ
π β§ π
β DivRing) β π β DivRing) |