MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ig1peu Structured version   Visualization version   GIF version

Theorem ig1peu 24222
Description: There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.)
Hypotheses
Ref Expression
ig1peu.p 𝑃 = (Poly1𝑅)
ig1peu.u 𝑈 = (LIdeal‘𝑃)
ig1peu.z 0 = (0g𝑃)
ig1peu.m 𝑀 = (Monic1p𝑅)
ig1peu.d 𝐷 = ( deg1𝑅)
Assertion
Ref Expression
ig1peu ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
Distinct variable groups:   𝐷,𝑔   𝑔,𝐼   𝑔,𝑀   𝑃,𝑔   𝑅,𝑔   𝑈,𝑔   0 ,𝑔

Proof of Theorem ig1peu
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2765 . . . . . . . . . . 11 (Base‘𝑃) = (Base‘𝑃)
2 ig1peu.u . . . . . . . . . . 11 𝑈 = (LIdeal‘𝑃)
31, 2lidlss 19484 . . . . . . . . . 10 (𝐼𝑈𝐼 ⊆ (Base‘𝑃))
433ad2ant2 1164 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝐼 ⊆ (Base‘𝑃))
54ssdifd 3908 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ⊆ ((Base‘𝑃) ∖ { 0 }))
6 imass2 5683 . . . . . . . 8 ((𝐼 ∖ { 0 }) ⊆ ((Base‘𝑃) ∖ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (𝐷 “ ((Base‘𝑃) ∖ { 0 })))
75, 6syl 17 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (𝐷 “ ((Base‘𝑃) ∖ { 0 })))
8 drngring 19023 . . . . . . . . 9 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
983ad2ant1 1163 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝑅 ∈ Ring)
10 ig1peu.d . . . . . . . . 9 𝐷 = ( deg1𝑅)
11 ig1peu.p . . . . . . . . 9 𝑃 = (Poly1𝑅)
12 ig1peu.z . . . . . . . . 9 0 = (0g𝑃)
1310, 11, 12, 1deg1n0ima 24140 . . . . . . . 8 (𝑅 ∈ Ring → (𝐷 “ ((Base‘𝑃) ∖ { 0 })) ⊆ ℕ0)
149, 13syl 17 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐷 “ ((Base‘𝑃) ∖ { 0 })) ⊆ ℕ0)
157, 14sstrd 3771 . . . . . 6 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ ℕ0)
16 nn0uz 11922 . . . . . 6 0 = (ℤ‘0)
1715, 16syl6sseq 3811 . . . . 5 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (ℤ‘0))
1811ply1ring 19891 . . . . . . . . . 10 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
199, 18syl 17 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝑃 ∈ Ring)
20 simp2 1167 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝐼𝑈)
212, 12lidl0cl 19486 . . . . . . . . 9 ((𝑃 ∈ Ring ∧ 𝐼𝑈) → 0𝐼)
2219, 20, 21syl2anc 579 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 0𝐼)
2322snssd 4494 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → { 0 } ⊆ 𝐼)
24 simp3 1168 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝐼 ≠ { 0 })
2524necomd 2992 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → { 0 } ≠ 𝐼)
26 pssdifn0 4108 . . . . . . 7 (({ 0 } ⊆ 𝐼 ∧ { 0 } ≠ 𝐼) → (𝐼 ∖ { 0 }) ≠ ∅)
2723, 25, 26syl2anc 579 . . . . . 6 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ≠ ∅)
2810, 11, 1deg1xrf 24132 . . . . . . . . . 10 𝐷:(Base‘𝑃)⟶ℝ*
29 ffn 6223 . . . . . . . . . 10 (𝐷:(Base‘𝑃)⟶ℝ*𝐷 Fn (Base‘𝑃))
3028, 29ax-mp 5 . . . . . . . . 9 𝐷 Fn (Base‘𝑃)
3130a1i 11 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝐷 Fn (Base‘𝑃))
324ssdifssd 3910 . . . . . . . 8 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ⊆ (Base‘𝑃))
33 fnimaeq0 6191 . . . . . . . 8 ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆ (Base‘𝑃)) → ((𝐷 “ (𝐼 ∖ { 0 })) = ∅ ↔ (𝐼 ∖ { 0 }) = ∅))
3431, 32, 33syl2anc 579 . . . . . . 7 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ((𝐷 “ (𝐼 ∖ { 0 })) = ∅ ↔ (𝐼 ∖ { 0 }) = ∅))
3534necon3bid 2981 . . . . . 6 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ((𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅ ↔ (𝐼 ∖ { 0 }) ≠ ∅))
3627, 35mpbird 248 . . . . 5 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅)
37 infssuzcl 11973 . . . . 5 (((𝐷 “ (𝐼 ∖ { 0 })) ⊆ (ℤ‘0) ∧ (𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ (𝐷 “ (𝐼 ∖ { 0 })))
3817, 36, 37syl2anc 579 . . . 4 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ (𝐷 “ (𝐼 ∖ { 0 })))
39 fvelimab 6442 . . . . 5 ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆ (Base‘𝑃)) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ (𝐷 “ (𝐼 ∖ { 0 })) ↔ ∃ ∈ (𝐼 ∖ { 0 })(𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
4031, 32, 39syl2anc 579 . . . 4 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ (𝐷 “ (𝐼 ∖ { 0 })) ↔ ∃ ∈ (𝐼 ∖ { 0 })(𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
4138, 40mpbid 223 . . 3 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ∃ ∈ (𝐼 ∖ { 0 })(𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
4219adantr 472 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → 𝑃 ∈ Ring)
43 simpl2 1244 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → 𝐼𝑈)
449adantr 472 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → 𝑅 ∈ Ring)
45 eqid 2765 . . . . . . . . . . 11 (algSc‘𝑃) = (algSc‘𝑃)
46 eqid 2765 . . . . . . . . . . 11 (Base‘𝑅) = (Base‘𝑅)
4711, 45, 46, 1ply1sclf 19928 . . . . . . . . . 10 (𝑅 ∈ Ring → (algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃))
4844, 47syl 17 . . . . . . . . 9 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → (algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃))
49 simpl1 1242 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → 𝑅 ∈ DivRing)
5032sselda 3761 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ∈ (Base‘𝑃))
51 eldifsni 4476 . . . . . . . . . . . . . 14 ( ∈ (𝐼 ∖ { 0 }) → 0 )
5251adantl 473 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → 0 )
53 eqid 2765 . . . . . . . . . . . . . 14 (Unic1p𝑅) = (Unic1p𝑅)
5411, 1, 12, 53drnguc1p 24221 . . . . . . . . . . . . 13 ((𝑅 ∈ DivRing ∧ ∈ (Base‘𝑃) ∧ 0 ) → ∈ (Unic1p𝑅))
5549, 50, 52, 54syl3anc 1490 . . . . . . . . . . . 12 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ∈ (Unic1p𝑅))
56 eqid 2765 . . . . . . . . . . . . 13 (Unit‘𝑅) = (Unit‘𝑅)
5710, 56, 53uc1pldg 24199 . . . . . . . . . . . 12 ( ∈ (Unic1p𝑅) → ((coe1)‘(𝐷)) ∈ (Unit‘𝑅))
5855, 57syl 17 . . . . . . . . . . 11 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ((coe1)‘(𝐷)) ∈ (Unit‘𝑅))
59 eqid 2765 . . . . . . . . . . . 12 (invr𝑅) = (invr𝑅)
6056, 59unitinvcl 18941 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ ((coe1)‘(𝐷)) ∈ (Unit‘𝑅)) → ((invr𝑅)‘((coe1)‘(𝐷))) ∈ (Unit‘𝑅))
6144, 58, 60syl2anc 579 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ((invr𝑅)‘((coe1)‘(𝐷))) ∈ (Unit‘𝑅))
6246, 56unitcl 18926 . . . . . . . . . 10 (((invr𝑅)‘((coe1)‘(𝐷))) ∈ (Unit‘𝑅) → ((invr𝑅)‘((coe1)‘(𝐷))) ∈ (Base‘𝑅))
6361, 62syl 17 . . . . . . . . 9 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ((invr𝑅)‘((coe1)‘(𝐷))) ∈ (Base‘𝑅))
6448, 63ffvelrnd 6550 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷)))) ∈ (Base‘𝑃))
65 eldifi 3894 . . . . . . . . 9 ( ∈ (𝐼 ∖ { 0 }) → 𝐼)
6665adantl 473 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → 𝐼)
67 eqid 2765 . . . . . . . . 9 (.r𝑃) = (.r𝑃)
682, 1, 67lidlmcl 19491 . . . . . . . 8 (((𝑃 ∈ Ring ∧ 𝐼𝑈) ∧ (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷)))) ∈ (Base‘𝑃) ∧ 𝐼)) → (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) ∈ 𝐼)
6942, 43, 64, 66, 68syl22anc 867 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) ∈ 𝐼)
70 ig1peu.m . . . . . . . . 9 𝑀 = (Monic1p𝑅)
7153, 70, 11, 67, 45, 10, 59uc1pmon1p 24202 . . . . . . . 8 ((𝑅 ∈ Ring ∧ ∈ (Unic1p𝑅)) → (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) ∈ 𝑀)
7244, 55, 71syl2anc 579 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) ∈ 𝑀)
7369, 72elind 3960 . . . . . 6 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) ∈ (𝐼𝑀))
74 eqid 2765 . . . . . . . . . 10 (RLReg‘𝑅) = (RLReg‘𝑅)
7574, 56unitrrg 19567 . . . . . . . . 9 (𝑅 ∈ Ring → (Unit‘𝑅) ⊆ (RLReg‘𝑅))
7644, 75syl 17 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → (Unit‘𝑅) ⊆ (RLReg‘𝑅))
7776, 61sseldd 3762 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ((invr𝑅)‘((coe1)‘(𝐷))) ∈ (RLReg‘𝑅))
7810, 11, 74, 1, 67, 45deg1mul3 24166 . . . . . . 7 ((𝑅 ∈ Ring ∧ ((invr𝑅)‘((coe1)‘(𝐷))) ∈ (RLReg‘𝑅) ∧ ∈ (Base‘𝑃)) → (𝐷‘(((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃))) = (𝐷))
7944, 77, 50, 78syl3anc 1490 . . . . . 6 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → (𝐷‘(((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃))) = (𝐷))
80 fveqeq2 6384 . . . . . . 7 (𝑔 = (((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) → ((𝐷𝑔) = (𝐷) ↔ (𝐷‘(((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃))) = (𝐷)))
8180rspcev 3461 . . . . . 6 (((((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃)) ∈ (𝐼𝑀) ∧ (𝐷‘(((algSc‘𝑃)‘((invr𝑅)‘((coe1)‘(𝐷))))(.r𝑃))) = (𝐷)) → ∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = (𝐷))
8273, 79, 81syl2anc 579 . . . . 5 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = (𝐷))
83 eqeq2 2776 . . . . . 6 ((𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) → ((𝐷𝑔) = (𝐷) ↔ (𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
8483rexbidv 3199 . . . . 5 ((𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) → (∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = (𝐷) ↔ ∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
8582, 84syl5ibcom 236 . . . 4 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ ∈ (𝐼 ∖ { 0 })) → ((𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) → ∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
8685rexlimdva 3178 . . 3 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (∃ ∈ (𝐼 ∖ { 0 })(𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) → ∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
8741, 86mpd 15 . 2 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
88 eqid 2765 . . . . . . 7 (-g𝑃) = (-g𝑃)
899ad2antrr 717 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) → 𝑅 ∈ Ring)
90 inss2 3993 . . . . . . . . 9 (𝐼𝑀) ⊆ 𝑀
91 simprl 787 . . . . . . . . 9 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑔 ∈ (𝐼𝑀))
9290, 91sseldi 3759 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑔𝑀)
9392adantr 472 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) → 𝑔𝑀)
94 simprl 787 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) → (𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
95 simprr 789 . . . . . . . . 9 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → ∈ (𝐼𝑀))
9690, 95sseldi 3759 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑀)
9796adantr 472 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) → 𝑀)
98 simprr 789 . . . . . . 7 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) → (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
9910, 70, 11, 88, 89, 93, 94, 97, 98deg1submon1p 24203 . . . . . 6 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))) → (𝐷‘(𝑔(-g𝑃))) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
10099ex 401 . . . . 5 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) → (𝐷‘(𝑔(-g𝑃))) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
10117ad2antrr 717 . . . . . . . . 9 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (ℤ‘0))
10230a1i 11 . . . . . . . . . 10 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → 𝐷 Fn (Base‘𝑃))
10332ad2antrr 717 . . . . . . . . . 10 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → (𝐼 ∖ { 0 }) ⊆ (Base‘𝑃))
10419adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑃 ∈ Ring)
105 simpl2 1244 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝐼𝑈)
106 inss1 3992 . . . . . . . . . . . . . 14 (𝐼𝑀) ⊆ 𝐼
107106, 91sseldi 3759 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑔𝐼)
108106, 95sseldi 3759 . . . . . . . . . . . . 13 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝐼)
1092, 88lidlsubcl 19490 . . . . . . . . . . . . 13 (((𝑃 ∈ Ring ∧ 𝐼𝑈) ∧ (𝑔𝐼𝐼)) → (𝑔(-g𝑃)) ∈ 𝐼)
110104, 105, 107, 108, 109syl22anc 867 . . . . . . . . . . . 12 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (𝑔(-g𝑃)) ∈ 𝐼)
111110adantr 472 . . . . . . . . . . 11 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → (𝑔(-g𝑃)) ∈ 𝐼)
112 simpr 477 . . . . . . . . . . 11 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → (𝑔(-g𝑃)) ≠ 0 )
113 eldifsn 4472 . . . . . . . . . . 11 ((𝑔(-g𝑃)) ∈ (𝐼 ∖ { 0 }) ↔ ((𝑔(-g𝑃)) ∈ 𝐼 ∧ (𝑔(-g𝑃)) ≠ 0 ))
114111, 112, 113sylanbrc 578 . . . . . . . . . 10 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → (𝑔(-g𝑃)) ∈ (𝐼 ∖ { 0 }))
115 fnfvima 6689 . . . . . . . . . 10 ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆ (Base‘𝑃) ∧ (𝑔(-g𝑃)) ∈ (𝐼 ∖ { 0 })) → (𝐷‘(𝑔(-g𝑃))) ∈ (𝐷 “ (𝐼 ∖ { 0 })))
116102, 103, 114, 115syl3anc 1490 . . . . . . . . 9 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → (𝐷‘(𝑔(-g𝑃))) ∈ (𝐷 “ (𝐼 ∖ { 0 })))
117 infssuzle 11972 . . . . . . . . 9 (((𝐷 “ (𝐼 ∖ { 0 })) ⊆ (ℤ‘0) ∧ (𝐷‘(𝑔(-g𝑃))) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤ (𝐷‘(𝑔(-g𝑃))))
118101, 116, 117syl2anc 579 . . . . . . . 8 ((((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) ∧ (𝑔(-g𝑃)) ≠ 0 ) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤ (𝐷‘(𝑔(-g𝑃))))
119118ex 401 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → ((𝑔(-g𝑃)) ≠ 0 → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤ (𝐷‘(𝑔(-g𝑃)))))
120 imassrn 5659 . . . . . . . . . . 11 (𝐷 “ (𝐼 ∖ { 0 })) ⊆ ran 𝐷
121 frn 6229 . . . . . . . . . . . 12 (𝐷:(Base‘𝑃)⟶ℝ* → ran 𝐷 ⊆ ℝ*)
12228, 121ax-mp 5 . . . . . . . . . . 11 ran 𝐷 ⊆ ℝ*
123120, 122sstri 3770 . . . . . . . . . 10 (𝐷 “ (𝐼 ∖ { 0 })) ⊆ ℝ*
124123, 38sseldi 3759 . . . . . . . . 9 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ ℝ*)
125124adantr 472 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ ℝ*)
126 ringgrp 18819 . . . . . . . . . . . 12 (𝑃 ∈ Ring → 𝑃 ∈ Grp)
12719, 126syl 17 . . . . . . . . . . 11 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → 𝑃 ∈ Grp)
128127adantr 472 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑃 ∈ Grp)
129106, 4syl5ss 3772 . . . . . . . . . . . 12 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → (𝐼𝑀) ⊆ (Base‘𝑃))
130129adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (𝐼𝑀) ⊆ (Base‘𝑃))
131130, 91sseldd 3762 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → 𝑔 ∈ (Base‘𝑃))
132130, 95sseldd 3762 . . . . . . . . . 10 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → ∈ (Base‘𝑃))
1331, 88grpsubcl 17764 . . . . . . . . . 10 ((𝑃 ∈ Grp ∧ 𝑔 ∈ (Base‘𝑃) ∧ ∈ (Base‘𝑃)) → (𝑔(-g𝑃)) ∈ (Base‘𝑃))
134128, 131, 132, 133syl3anc 1490 . . . . . . . . 9 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (𝑔(-g𝑃)) ∈ (Base‘𝑃))
13510, 11, 1deg1xrcl 24133 . . . . . . . . 9 ((𝑔(-g𝑃)) ∈ (Base‘𝑃) → (𝐷‘(𝑔(-g𝑃))) ∈ ℝ*)
136134, 135syl 17 . . . . . . . 8 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (𝐷‘(𝑔(-g𝑃))) ∈ ℝ*)
137 xrlenlt 10357 . . . . . . . 8 ((inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∈ ℝ* ∧ (𝐷‘(𝑔(-g𝑃))) ∈ ℝ*) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤ (𝐷‘(𝑔(-g𝑃))) ↔ ¬ (𝐷‘(𝑔(-g𝑃))) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
138125, 136, 137syl2anc 579 . . . . . . 7 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤ (𝐷‘(𝑔(-g𝑃))) ↔ ¬ (𝐷‘(𝑔(-g𝑃))) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
139119, 138sylibd 230 . . . . . 6 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → ((𝑔(-g𝑃)) ≠ 0 → ¬ (𝐷‘(𝑔(-g𝑃))) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
140139necon4ad 2956 . . . . 5 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → ((𝐷‘(𝑔(-g𝑃))) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) → (𝑔(-g𝑃)) = 0 ))
141100, 140syld 47 . . . 4 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) → (𝑔(-g𝑃)) = 0 ))
1421, 12, 88grpsubeq0 17770 . . . . 5 ((𝑃 ∈ Grp ∧ 𝑔 ∈ (Base‘𝑃) ∧ ∈ (Base‘𝑃)) → ((𝑔(-g𝑃)) = 0𝑔 = ))
143128, 131, 132, 142syl3anc 1490 . . . 4 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → ((𝑔(-g𝑃)) = 0𝑔 = ))
144141, 143sylibd 230 . . 3 (((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼𝑀) ∧ ∈ (𝐼𝑀))) → (((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) → 𝑔 = ))
145144ralrimivva 3118 . 2 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ∀𝑔 ∈ (𝐼𝑀)∀ ∈ (𝐼𝑀)(((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) → 𝑔 = ))
146 fveqeq2 6384 . . 3 (𝑔 = → ((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ↔ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
147146reu4 3559 . 2 (∃!𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ↔ (∃𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ ∀𝑔 ∈ (𝐼𝑀)∀ ∈ (𝐼𝑀)(((𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧ (𝐷) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )) → 𝑔 = )))
14887, 145, 147sylanbrc 578 1 ((𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼𝑀)(𝐷𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  ∃!wreu 3057  cdif 3729  cin 3731  wss 3732  c0 4079  {csn 4334   class class class wbr 4809  ran crn 5278  cima 5280   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  infcinf 8554  cr 10188  0cc0 10189  *cxr 10327   < clt 10328  cle 10329  0cn0 11538  cuz 11886  Basecbs 16132  .rcmulr 16217  0gc0g 16368  Grpcgrp 17691  -gcsg 17693  Ringcrg 18814  Unitcui 18906  invrcinvr 18938  DivRingcdr 19016  LIdealclidl 19444  RLRegcrlreg 19553  algSccascl 19585  Poly1cpl1 19820  coe1cco1 19821   deg1 cdg1 24105  Monic1pcmn1 24176  Unic1pcuc1p 24177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-ofr 7096  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-tpos 7555  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-fz 12534  df-fzo 12674  df-seq 13009  df-hash 13322  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-starv 16231  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-unif 16239  df-0g 16370  df-gsum 16371  df-mre 16514  df-mrc 16515  df-acs 16517  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-mhm 17603  df-submnd 17604  df-grp 17694  df-minusg 17695  df-sbg 17696  df-mulg 17810  df-subg 17857  df-ghm 17924  df-cntz 18015  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-cring 18817  df-oppr 18890  df-dvdsr 18908  df-unit 18909  df-invr 18939  df-drng 19018  df-subrg 19047  df-lmod 19134  df-lss 19202  df-sra 19446  df-rgmod 19447  df-lidl 19448  df-rlreg 19557  df-ascl 19588  df-psr 19630  df-mvr 19631  df-mpl 19632  df-opsr 19634  df-psr1 19823  df-vr1 19824  df-ply1 19825  df-coe1 19826  df-cnfld 20020  df-mdeg 24106  df-deg1 24107  df-mon1 24181  df-uc1p 24182
This theorem is referenced by:  ig1pval3  24225
  Copyright terms: Public domain W3C validator