Step | Hyp | Ref
| Expression |
1 | | qsdrng.q |
. . . 4
β’ π = (π
/s (π
~QG π)) |
2 | | eqid 2731 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | qsdrng.r |
. . . . 5
β’ (π β π
β NzRing) |
4 | | nzrring 20408 |
. . . . 5
β’ (π
β NzRing β π
β Ring) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β π
β Ring) |
6 | | qsdrngi.1 |
. . . . . . 7
β’ (π β π β (MaxIdealβπ
)) |
7 | 2 | mxidlidl 32854 |
. . . . . . 7
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β π β (LIdealβπ
)) |
8 | 5, 6, 7 | syl2anc 583 |
. . . . . 6
β’ (π β π β (LIdealβπ
)) |
9 | | qsdrng.0 |
. . . . . . . . 9
β’ π =
(opprβπ
) |
10 | 9 | opprring 20239 |
. . . . . . . 8
β’ (π
β Ring β π β Ring) |
11 | 5, 10 | syl 17 |
. . . . . . 7
β’ (π β π β Ring) |
12 | | qsdrngi.2 |
. . . . . . 7
β’ (π β π β (MaxIdealβπ)) |
13 | | eqid 2731 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
14 | 13 | mxidlidl 32854 |
. . . . . . 7
β’ ((π β Ring β§ π β (MaxIdealβπ)) β π β (LIdealβπ)) |
15 | 11, 12, 14 | syl2anc 583 |
. . . . . 6
β’ (π β π β (LIdealβπ)) |
16 | 8, 15 | elind 4194 |
. . . . 5
β’ (π β π β ((LIdealβπ
) β© (LIdealβπ))) |
17 | | eqid 2731 |
. . . . . 6
β’
(LIdealβπ
) =
(LIdealβπ
) |
18 | | eqid 2731 |
. . . . . 6
β’
(LIdealβπ) =
(LIdealβπ) |
19 | | eqid 2731 |
. . . . . 6
β’
(2Idealβπ
) =
(2Idealβπ
) |
20 | 17, 9, 18, 19 | 2idlval 21008 |
. . . . 5
β’
(2Idealβπ
) =
((LIdealβπ
) β©
(LIdealβπ)) |
21 | 16, 20 | eleqtrrdi 2843 |
. . . 4
β’ (π β π β (2Idealβπ
)) |
22 | 2 | mxidlnr 32855 |
. . . . 5
β’ ((π
β Ring β§ π β (MaxIdealβπ
)) β π β (Baseβπ
)) |
23 | 5, 6, 22 | syl2anc 583 |
. . . 4
β’ (π β π β (Baseβπ
)) |
24 | 1, 2, 5, 3, 21, 23 | qsnzr 32849 |
. . 3
β’ (π β π β NzRing) |
25 | | eqid 2731 |
. . . 4
β’
(1rβπ) = (1rβπ) |
26 | | eqid 2731 |
. . . 4
β’
(0gβπ) = (0gβπ) |
27 | 25, 26 | nzrnz 20407 |
. . 3
β’ (π β NzRing β
(1rβπ)
β (0gβπ)) |
28 | 24, 27 | syl 17 |
. 2
β’ (π β (1rβπ) β
(0gβπ)) |
29 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
30 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’
(.rβπ) = (.rβπ) |
31 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’
(Unitβπ) =
(Unitβπ) |
32 | 1, 19 | qusring 21024 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Ring β§ π β (2Idealβπ
)) β π β Ring) |
33 | 5, 21, 32 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
β’ (π β π β Ring) |
34 | 33 | ad10antr 741 |
. . . . . . . . . . . . . . 15
β’
(((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β π β Ring) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π β Ring) |
36 | | eldifi 4126 |
. . . . . . . . . . . . . . . 16
β’ (π’ β ((Baseβπ) β
{(0gβπ)})
β π’ β
(Baseβπ)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β π’ β (Baseβπ)) |
38 | 37 | ad10antr 741 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π’ β (Baseβπ)) |
39 | | ovex 7445 |
. . . . . . . . . . . . . . . . 17
β’ (π
~QG π) β V |
40 | 39 | ecelqsi 8770 |
. . . . . . . . . . . . . . . 16
β’ (π β (Baseβπ
) β [π](π
~QG π) β ((Baseβπ
) / (π
~QG π))) |
41 | 40 | ad4antlr 730 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π](π
~QG π) β ((Baseβπ
) / (π
~QG π))) |
42 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π = (π
/s (π
~QG π))) |
43 | | eqidd 2732 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Baseβπ
) = (Baseβπ
)) |
44 | | ovexd 7447 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π
~QG π) β V) |
45 | 42, 43, 44, 3 | qusbas 17496 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((Baseβπ
) / (π
~QG π)) = (Baseβπ)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β ((Baseβπ
) / (π
~QG π)) = (Baseβπ)) |
47 | 46 | ad10antr 741 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β ((Baseβπ
) / (π
~QG π)) = (Baseβπ)) |
48 | 41, 47 | eleqtrd 2834 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π](π
~QG π) β (Baseβπ)) |
49 | 39 | ecelqsi 8770 |
. . . . . . . . . . . . . . . 16
β’ (π β (Baseβπ
) β [π ](π
~QG π) β ((Baseβπ
) / (π
~QG π))) |
50 | 49 | ad2antlr 724 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π ](π
~QG π) β ((Baseβπ
) / (π
~QG π))) |
51 | 50, 47 | eleqtrd 2834 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π ](π
~QG π) β (Baseβπ)) |
52 | | simpllr 773 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π£ = [π](π
~QG π)) |
53 | | simp-9r 791 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π’ = [π₯](π
~QG π)) |
54 | 53 | eqcomd 2737 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π₯](π
~QG π) = π’) |
55 | 52, 54 | oveq12d 7430 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π£(.rβπ)[π₯](π
~QG π)) = ([π](π
~QG π)(.rβπ)π’)) |
56 | | simp-7r 787 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) |
57 | 55, 56 | eqtr3d 2773 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β ([π](π
~QG π)(.rβπ)π’) = (1rβπ)) |
58 | | eqid 2731 |
. . . . . . . . . . . . . . . 16
β’
(opprβπ) = (opprβπ) |
59 | | eqid 2731 |
. . . . . . . . . . . . . . . 16
β’
(.rβ(opprβπ)) =
(.rβ(opprβπ)) |
60 | 29, 30, 58, 59 | opprmul 20229 |
. . . . . . . . . . . . . . 15
β’ ([π ](π
~QG π)(.rβ(opprβπ))π’) = (π’(.rβπ)[π ](π
~QG π)) |
61 | | simp-5r 783 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) |
62 | 5 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π
β Ring) |
63 | 62 | ad8antr 737 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π
β Ring) |
64 | 21 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π β (2Idealβπ
)) |
65 | 64 | ad8antr 737 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π β (2Idealβπ
)) |
66 | 2, 9, 1, 63, 65, 29, 51, 38 | opprqusmulr 32880 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β ([π ](π
~QG π)(.rβ(opprβπ))π’) = ([π ](π
~QG π)(.rβ(π /s (π ~QG π)))π’)) |
67 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π€ = [π ](π
~QG π)) |
68 | 2, 17 | lidlss 20979 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (LIdealβπ
) β π β (Baseβπ
)) |
69 | 8, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β (Baseβπ
)) |
70 | 9, 2 | oppreqg 32872 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π
β Ring β§ π β (Baseβπ
)) β (π
~QG π) = (π ~QG π)) |
71 | 5, 69, 70 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π
~QG π) = (π ~QG π)) |
72 | 71 | ad10antr 741 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β (π
~QG π) = (π ~QG π)) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π
~QG π) = (π ~QG π)) |
74 | 73 | eceq2d 8748 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π₯](π
~QG π) = [π₯](π ~QG π)) |
75 | 53, 74 | eqtr2d 2772 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π₯](π ~QG π) = π’) |
76 | 67, 75 | oveq12d 7430 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = ([π ](π
~QG π)(.rβ(π /s (π ~QG π)))π’)) |
77 | 66, 76 | eqtr4d 2774 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β ([π ](π
~QG π)(.rβ(opprβπ))π’) = (π€(.rβ(π /s (π ~QG π)))[π₯](π
~QG π))) |
78 | 58, 25 | oppr1 20242 |
. . . . . . . . . . . . . . . . . . 19
β’
(1rβπ) =
(1rβ(opprβπ)) |
79 | 2, 9, 1, 5, 21 | opprqus1r 32881 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(1rβ(opprβπ)) = (1rβ(π /s (π ~QG π)))) |
80 | 78, 79 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1rβπ) = (1rβ(π /s (π ~QG π)))) |
81 | 80 | ad10antr 741 |
. . . . . . . . . . . . . . . . 17
β’
(((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β (1rβπ) = (1rβ(π /s (π ~QG π)))) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (1rβπ) = (1rβ(π /s (π ~QG π)))) |
83 | 61, 77, 82 | 3eqtr4d 2781 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β ([π ](π
~QG π)(.rβ(opprβπ))π’) = (1rβπ)) |
84 | 60, 83 | eqtr3id 2785 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π’(.rβπ)[π ](π
~QG π)) = (1rβπ)) |
85 | 29, 26, 25, 30, 31, 35, 38, 48, 51, 57, 84 | ringinveu 32665 |
. . . . . . . . . . . . 13
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β [π ](π
~QG π) = [π](π
~QG π)) |
86 | 85, 67, 52 | 3eqtr4rd 2782 |
. . . . . . . . . . . 12
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β π£ = π€) |
87 | 86 | oveq2d 7428 |
. . . . . . . . . . 11
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π’(.rβπ)π£) = (π’(.rβπ)π€)) |
88 | 67 | oveq2d 7428 |
. . . . . . . . . . 11
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π’(.rβπ)π€) = (π’(.rβπ)[π ](π
~QG π))) |
89 | 87, 88, 84 | 3eqtrd 2775 |
. . . . . . . . . 10
β’
((((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β§ π β (Baseβπ
)) β§ π€ = [π ](π
~QG π)) β (π’(.rβπ)π£) = (1rβπ)) |
90 | | simp-4r 781 |
. . . . . . . . . . . 12
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β π€ β (Baseβ(π /s (π ~QG π)))) |
91 | 71 | qseq2d 8763 |
. . . . . . . . . . . . . 14
β’ (π β ((Baseβπ
) / (π
~QG π)) = ((Baseβπ
) / (π ~QG π))) |
92 | 91 | ad9antr 739 |
. . . . . . . . . . . . 13
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β ((Baseβπ
) / (π
~QG π)) = ((Baseβπ
) / (π ~QG π))) |
93 | | eqidd 2732 |
. . . . . . . . . . . . . 14
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β (π /s (π ~QG π)) = (π /s (π ~QG π))) |
94 | 9, 2 | opprbas 20233 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ
) =
(Baseβπ) |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β (Baseβπ
) = (Baseβπ)) |
96 | | ovexd 7447 |
. . . . . . . . . . . . . 14
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β (π ~QG π) β V) |
97 | 9 | fvexi 6905 |
. . . . . . . . . . . . . . 15
β’ π β V |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β π β V) |
99 | 93, 95, 96, 98 | qusbas 17496 |
. . . . . . . . . . . . 13
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β ((Baseβπ
) / (π ~QG π)) = (Baseβ(π /s (π ~QG π)))) |
100 | 92, 99 | eqtr2d 2772 |
. . . . . . . . . . . 12
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β (Baseβ(π /s (π ~QG π))) = ((Baseβπ
) / (π
~QG π))) |
101 | 90, 100 | eleqtrd 2834 |
. . . . . . . . . . 11
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β π€ β ((Baseβπ
) / (π
~QG π))) |
102 | | elqsi 8767 |
. . . . . . . . . . 11
β’ (π€ β ((Baseβπ
) / (π
~QG π)) β βπ β (Baseβπ
)π€ = [π ](π
~QG π)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β βπ β (Baseβπ
)π€ = [π ](π
~QG π)) |
104 | 89, 103 | r19.29a 3161 |
. . . . . . . . 9
β’
((((((((((π β§
π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β§ π β (Baseβπ
)) β§ π£ = [π](π
~QG π)) β (π’(.rβπ)π£) = (1rβπ)) |
105 | | simp-4r 781 |
. . . . . . . . . . 11
β’
((((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β π£ β (Baseβπ)) |
106 | 46 | ad6antr 733 |
. . . . . . . . . . 11
β’
((((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β ((Baseβπ
) / (π
~QG π)) = (Baseβπ)) |
107 | 105, 106 | eleqtrrd 2835 |
. . . . . . . . . 10
β’
((((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β π£ β ((Baseβπ
) / (π
~QG π))) |
108 | | elqsi 8767 |
. . . . . . . . . 10
β’ (π£ β ((Baseβπ
) / (π
~QG π)) β βπ β (Baseβπ
)π£ = [π](π
~QG π)) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
β’
((((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β βπ β (Baseβπ
)π£ = [π](π
~QG π)) |
110 | 104, 109 | r19.29a 3161 |
. . . . . . . 8
β’
((((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β§ π€ β (Baseβ(π /s (π ~QG π)))) β§ (π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) β (π’(.rβπ)π£) = (1rβπ)) |
111 | | eqid 2731 |
. . . . . . . . . 10
β’
(opprβπ) = (opprβπ) |
112 | | eqid 2731 |
. . . . . . . . . 10
β’ (π /s (π ~QG π)) = (π /s (π ~QG π)) |
113 | 3 | ad3antrrr 727 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π
β NzRing) |
114 | 9 | opprnzr 20412 |
. . . . . . . . . . 11
β’ (π
β NzRing β π β NzRing) |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π β NzRing) |
116 | 12 | ad3antrrr 727 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π β (MaxIdealβπ)) |
117 | 6 | ad3antrrr 727 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π β (MaxIdealβπ
)) |
118 | 9, 62, 117 | opprmxidlabs 32876 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π β
(MaxIdealβ(opprβπ))) |
119 | | simplr 766 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π₯ β (Baseβπ
)) |
120 | 94 | a1i 11 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β (Baseβπ
) = (Baseβπ)) |
121 | 119, 120 | eleqtrd 2834 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β π₯ β (Baseβπ)) |
122 | | simplr 766 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β π’ = [π₯](π
~QG π)) |
123 | 5 | ringgrpd 20137 |
. . . . . . . . . . . . . . 15
β’ (π β π
β Grp) |
124 | 123 | ad4antr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β π
β Grp) |
125 | | lidlnsg 32839 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Ring β§ π β (LIdealβπ
)) β π β (NrmSGrpβπ
)) |
126 | 5, 8, 125 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (NrmSGrpβπ
)) |
127 | | nsgsubg 19075 |
. . . . . . . . . . . . . . . 16
β’ (π β (NrmSGrpβπ
) β π β (SubGrpβπ
)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β (SubGrpβπ
)) |
129 | 128 | ad4antr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β π β (SubGrpβπ
)) |
130 | | simpr 484 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β π₯ β π) |
131 | | eqid 2731 |
. . . . . . . . . . . . . . . 16
β’ (π
~QG π) = (π
~QG π) |
132 | 131 | eqg0el 32748 |
. . . . . . . . . . . . . . 15
β’ ((π
β Grp β§ π β (SubGrpβπ
)) β ([π₯](π
~QG π) = π β π₯ β π)) |
133 | 132 | biimpar 477 |
. . . . . . . . . . . . . 14
β’ (((π
β Grp β§ π β (SubGrpβπ
)) β§ π₯ β π) β [π₯](π
~QG π) = π) |
134 | 124, 129,
130, 133 | syl21anc 835 |
. . . . . . . . . . . . 13
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β [π₯](π
~QG π) = π) |
135 | | eqid 2731 |
. . . . . . . . . . . . . . 15
β’
(0gβπ
) = (0gβπ
) |
136 | 2, 131, 135 | eqgid 19097 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπ
) β
[(0gβπ
)](π
~QG π) = π) |
137 | 129, 136 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β [(0gβπ
)](π
~QG π) = π) |
138 | 134, 137 | eqtr4d 2774 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β [π₯](π
~QG π) = [(0gβπ
)](π
~QG π)) |
139 | 1, 135 | qus0 19105 |
. . . . . . . . . . . . . 14
β’ (π β (NrmSGrpβπ
) β
[(0gβπ
)](π
~QG π) = (0gβπ)) |
140 | 126, 139 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β
[(0gβπ
)](π
~QG π) = (0gβπ)) |
141 | 140 | ad4antr 729 |
. . . . . . . . . . . 12
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β [(0gβπ
)](π
~QG π) = (0gβπ)) |
142 | 122, 138,
141 | 3eqtrd 2775 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β π’ = (0gβπ)) |
143 | | eldifsnneq 4794 |
. . . . . . . . . . . 12
β’ (π’ β ((Baseβπ) β
{(0gβπ)})
β Β¬ π’ =
(0gβπ)) |
144 | 143 | ad4antlr 730 |
. . . . . . . . . . 11
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π₯ β π) β Β¬ π’ = (0gβπ)) |
145 | 142, 144 | pm2.65da 814 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β Β¬ π₯ β π) |
146 | 111, 112,
115, 116, 118, 121, 145 | qsdrngilem 32883 |
. . . . . . . . 9
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β βπ€ β (Baseβ(π /s (π ~QG π)))(π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) |
147 | 146 | ad2antrr 723 |
. . . . . . . 8
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β βπ€ β (Baseβ(π /s (π ~QG π)))(π€(.rβ(π /s (π ~QG π)))[π₯](π ~QG π)) = (1rβ(π /s (π ~QG π)))) |
148 | 110, 147 | r19.29a 3161 |
. . . . . . 7
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β (π’(.rβπ)π£) = (1rβπ)) |
149 | | simpllr 773 |
. . . . . . . . 9
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β π’ = [π₯](π
~QG π)) |
150 | 149 | oveq2d 7428 |
. . . . . . . 8
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β (π£(.rβπ)π’) = (π£(.rβπ)[π₯](π
~QG π))) |
151 | | simpr 484 |
. . . . . . . 8
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) |
152 | 150, 151 | eqtrd 2771 |
. . . . . . 7
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β (π£(.rβπ)π’) = (1rβπ)) |
153 | 148, 152 | jca 511 |
. . . . . 6
β’
((((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ π£ β (Baseβπ)) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) β ((π’(.rβπ)π£) = (1rβπ) β§ (π£(.rβπ)π’) = (1rβπ))) |
154 | 153 | anasss 466 |
. . . . 5
β’
(((((π β§ π’ β ((Baseβπ) β
{(0gβπ)}))
β§ π₯ β
(Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β§ (π£ β (Baseβπ) β§ (π£(.rβπ)[π₯](π
~QG π)) = (1rβπ))) β ((π’(.rβπ)π£) = (1rβπ) β§ (π£(.rβπ)π’) = (1rβπ))) |
155 | 9, 1, 113, 117, 116, 119, 145 | qsdrngilem 32883 |
. . . . 5
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β βπ£ β (Baseβπ)(π£(.rβπ)[π₯](π
~QG π)) = (1rβπ)) |
156 | 154, 155 | reximddv 3170 |
. . . 4
β’ ((((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β§ π₯ β (Baseβπ
)) β§ π’ = [π₯](π
~QG π)) β βπ£ β (Baseβπ)((π’(.rβπ)π£) = (1rβπ) β§ (π£(.rβπ)π’) = (1rβπ))) |
157 | 37, 46 | eleqtrrd 2835 |
. . . . 5
β’ ((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β π’ β ((Baseβπ
) / (π
~QG π))) |
158 | | elqsi 8767 |
. . . . 5
β’ (π’ β ((Baseβπ
) / (π
~QG π)) β βπ₯ β (Baseβπ
)π’ = [π₯](π
~QG π)) |
159 | 157, 158 | syl 17 |
. . . 4
β’ ((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β βπ₯ β (Baseβπ
)π’ = [π₯](π
~QG π)) |
160 | 156, 159 | r19.29a 3161 |
. . 3
β’ ((π β§ π’ β ((Baseβπ) β {(0gβπ)})) β βπ£ β (Baseβπ)((π’(.rβπ)π£) = (1rβπ) β§ (π£(.rβπ)π’) = (1rβπ))) |
161 | 160 | ralrimiva 3145 |
. 2
β’ (π β βπ’ β ((Baseβπ) β {(0gβπ)})βπ£ β (Baseβπ)((π’(.rβπ)π£) = (1rβπ) β§ (π£(.rβπ)π’) = (1rβπ))) |
162 | 29, 26, 25, 30, 31, 33 | isdrng4 32666 |
. 2
β’ (π β (π β DivRing β
((1rβπ)
β (0gβπ) β§ βπ’ β ((Baseβπ) β {(0gβπ)})βπ£ β (Baseβπ)((π’(.rβπ)π£) = (1rβπ) β§ (π£(.rβπ)π’) = (1rβπ))))) |
163 | 28, 161, 162 | mpbir2and 710 |
1
β’ (π β π β DivRing) |