| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 2 | | ig1peu.u |
. . . . . . . . . . 11
⊢ 𝑈 = (LIdeal‘𝑃) |
| 3 | 1, 2 | lidlss 21222 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑈 → 𝐼 ⊆ (Base‘𝑃)) |
| 4 | 3 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐼 ⊆ (Base‘𝑃)) |
| 5 | 4 | ssdifd 4145 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ⊆
((Base‘𝑃) ∖ {
0
})) |
| 6 | | imass2 6120 |
. . . . . . . 8
⊢ ((𝐼 ∖ { 0 }) ⊆
((Base‘𝑃) ∖ {
0 })
→ (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (𝐷 “ ((Base‘𝑃) ∖ { 0 }))) |
| 7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (𝐷 “ ((Base‘𝑃) ∖ { 0 }))) |
| 8 | | drngring 20736 |
. . . . . . . . 9
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
| 9 | 8 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝑅 ∈ Ring) |
| 10 | | ig1peu.d |
. . . . . . . . 9
⊢ 𝐷 = (deg1‘𝑅) |
| 11 | | ig1peu.p |
. . . . . . . . 9
⊢ 𝑃 = (Poly1‘𝑅) |
| 12 | | ig1peu.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑃) |
| 13 | 10, 11, 12, 1 | deg1n0ima 26128 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (𝐷 “ ((Base‘𝑃) ∖ { 0 })) ⊆
ℕ0) |
| 14 | 9, 13 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ ((Base‘𝑃) ∖ { 0 })) ⊆
ℕ0) |
| 15 | 7, 14 | sstrd 3994 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆
ℕ0) |
| 16 | | nn0uz 12920 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
| 17 | 15, 16 | sseqtrdi 4024 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0)) |
| 18 | 11 | ply1ring 22249 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 19 | 9, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝑃 ∈ Ring) |
| 20 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐼 ∈ 𝑈) |
| 21 | 2, 12 | lidl0cl 21230 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼) |
| 22 | 19, 20, 21 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 0 ∈ 𝐼) |
| 23 | 22 | snssd 4809 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → { 0 } ⊆
𝐼) |
| 24 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐼 ≠ { 0 }) |
| 25 | 24 | necomd 2996 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → { 0 } ≠ 𝐼) |
| 26 | | pssdifn0 4368 |
. . . . . . 7
⊢ (({ 0 } ⊆
𝐼 ∧ { 0 } ≠ 𝐼) → (𝐼 ∖ { 0 }) ≠
∅) |
| 27 | 23, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ≠
∅) |
| 28 | 10, 11, 1 | deg1xrf 26120 |
. . . . . . . . . 10
⊢ 𝐷:(Base‘𝑃)⟶ℝ* |
| 29 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝐷:(Base‘𝑃)⟶ℝ* → 𝐷 Fn (Base‘𝑃)) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐷 Fn (Base‘𝑃) |
| 31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐷 Fn (Base‘𝑃)) |
| 32 | 4 | ssdifssd 4147 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) |
| 33 | | fnimaeq0 6701 |
. . . . . . . 8
⊢ ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) →
((𝐷 “ (𝐼 ∖ { 0 })) = ∅ ↔
(𝐼 ∖ { 0 }) =
∅)) |
| 34 | 31, 32, 33 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐷 “ (𝐼 ∖ { 0 })) = ∅ ↔
(𝐼 ∖ { 0 }) =
∅)) |
| 35 | 34 | necon3bid 2985 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅ ↔
(𝐼 ∖ { 0 }) ≠
∅)) |
| 36 | 27, 35 | mpbird 257 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ≠
∅) |
| 37 | | infssuzcl 12974 |
. . . . 5
⊢ (((𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0) ∧ (𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅) →
inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
| 38 | 17, 36, 37 | syl2anc 584 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
| 39 | 31, 32 | fvelimabd 6982 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 })) ↔ ∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 40 | 38, 39 | mpbid 232 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
| 41 | 19 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝑃 ∈ Ring) |
| 42 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝐼 ∈ 𝑈) |
| 43 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝑅 ∈ Ring) |
| 44 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
| 45 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 46 | 11, 44, 45, 1 | ply1sclf 22288 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃)) |
| 47 | 43, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃)) |
| 48 | | simpl1 1192 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝑅 ∈
DivRing) |
| 49 | 32 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ∈ (Base‘𝑃)) |
| 50 | | eldifsni 4790 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝐼 ∖ { 0 }) → ℎ ≠ 0 ) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ≠ 0 ) |
| 52 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
| 53 | 11, 1, 12, 52 | drnguc1p 26213 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ ℎ ∈ (Base‘𝑃) ∧ ℎ ≠ 0 ) → ℎ ∈
(Unic1p‘𝑅)) |
| 54 | 48, 49, 51, 53 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ∈
(Unic1p‘𝑅)) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 56 | 10, 55, 52 | uc1pldg 26188 |
. . . . . . . . . . . 12
⊢ (ℎ ∈
(Unic1p‘𝑅)
→ ((coe1‘ℎ)‘(𝐷‘ℎ)) ∈ (Unit‘𝑅)) |
| 57 | 54, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((coe1‘ℎ)‘(𝐷‘ℎ)) ∈ (Unit‘𝑅)) |
| 58 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(invr‘𝑅) = (invr‘𝑅) |
| 59 | 55, 58 | unitinvcl 20390 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
((coe1‘ℎ)‘(𝐷‘ℎ)) ∈ (Unit‘𝑅)) → ((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Unit‘𝑅)) |
| 60 | 43, 57, 59 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Unit‘𝑅)) |
| 61 | 45, 55 | unitcl 20375 |
. . . . . . . . . 10
⊢
(((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Unit‘𝑅) → ((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Base‘𝑅)) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Base‘𝑅)) |
| 63 | 47, 62 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ)))) ∈ (Base‘𝑃)) |
| 64 | | eldifi 4131 |
. . . . . . . . 9
⊢ (ℎ ∈ (𝐼 ∖ { 0 }) → ℎ ∈ 𝐼) |
| 65 | 64 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ∈ 𝐼) |
| 66 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 67 | 2, 1, 66 | lidlmcl 21235 |
. . . . . . . 8
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ)))) ∈ (Base‘𝑃) ∧ ℎ ∈ 𝐼)) → (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝐼) |
| 68 | 41, 42, 63, 65, 67 | syl22anc 839 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝐼) |
| 69 | | ig1peu.m |
. . . . . . . . 9
⊢ 𝑀 =
(Monic1p‘𝑅) |
| 70 | 52, 69, 11, 66, 44, 10, 58 | uc1pmon1p 26191 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ ℎ ∈
(Unic1p‘𝑅)) → (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝑀) |
| 71 | 43, 54, 70 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝑀) |
| 72 | 68, 71 | elind 4200 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ (𝐼 ∩ 𝑀)) |
| 73 | | eqid 2737 |
. . . . . . . . . 10
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) |
| 74 | 73, 55 | unitrrg 20703 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
| 75 | 43, 74 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
| 76 | 75, 60 | sseldd 3984 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (RLReg‘𝑅)) |
| 77 | 10, 11, 73, 1, 66, 44 | deg1mul3 26155 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (RLReg‘𝑅) ∧ ℎ ∈ (Base‘𝑃)) → (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ)) |
| 78 | 43, 76, 49, 77 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ)) |
| 79 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑔 = (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) → ((𝐷‘𝑔) = (𝐷‘ℎ) ↔ (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ))) |
| 80 | 79 | rspcev 3622 |
. . . . . 6
⊢
(((((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ (𝐼 ∩ 𝑀) ∧ (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ)) → ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = (𝐷‘ℎ)) |
| 81 | 72, 78, 80 | syl2anc 584 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = (𝐷‘ℎ)) |
| 82 | | eqeq2 2749 |
. . . . . 6
⊢ ((𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ ((𝐷‘𝑔) = (𝐷‘ℎ) ↔ (𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 83 | 82 | rexbidv 3179 |
. . . . 5
⊢ ((𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ (∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = (𝐷‘ℎ) ↔ ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 84 | 81, 83 | syl5ibcom 245 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ((𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ ∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 85 | 84 | rexlimdva 3155 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ ∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 86 | 40, 85 | mpd 15 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
| 87 | | eqid 2737 |
. . . . . . 7
⊢
(-g‘𝑃) = (-g‘𝑃) |
| 88 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ 𝑅 ∈
Ring) |
| 89 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ (𝐼 ∩ 𝑀)) |
| 90 | 89 | elin2d 4205 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ 𝑀) |
| 91 | 90 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ 𝑔 ∈ 𝑀) |
| 92 | | simprl 771 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ (𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
| 93 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ (𝐼 ∩ 𝑀)) |
| 94 | 93 | elin2d 4205 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ 𝑀) |
| 95 | 94 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ ℎ ∈ 𝑀) |
| 96 | | simprr 773 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ (𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
| 97 | 10, 69, 11, 87, 88, 91, 92, 95, 96 | deg1submon1p 26192 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
| 98 | 97 | ex 412 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 99 | 17 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0)) |
| 100 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → 𝐷 Fn (Base‘𝑃)) |
| 101 | 32 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) |
| 102 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑃 ∈ Ring) |
| 103 | | simpl2 1193 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝐼 ∈ 𝑈) |
| 104 | 89 | elin1d 4204 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ 𝐼) |
| 105 | 93 | elin1d 4204 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ 𝐼) |
| 106 | 2, 87 | lidlsubcl 21234 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑔 ∈ 𝐼 ∧ ℎ ∈ 𝐼)) → (𝑔(-g‘𝑃)ℎ) ∈ 𝐼) |
| 107 | 102, 103,
104, 105, 106 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝑔(-g‘𝑃)ℎ) ∈ 𝐼) |
| 108 | 107 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝑔(-g‘𝑃)ℎ) ∈ 𝐼) |
| 109 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝑔(-g‘𝑃)ℎ) ≠ 0 ) |
| 110 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢ ((𝑔(-g‘𝑃)ℎ) ∈ (𝐼 ∖ { 0 }) ↔ ((𝑔(-g‘𝑃)ℎ) ∈ 𝐼 ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 )) |
| 111 | 108, 109,
110 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝑔(-g‘𝑃)ℎ) ∈ (𝐼 ∖ { 0 })) |
| 112 | | fnfvima 7253 |
. . . . . . . . . 10
⊢ ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃) ∧ (𝑔(-g‘𝑃)ℎ) ∈ (𝐼 ∖ { 0 })) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
| 113 | 100, 101,
111, 112 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
| 114 | | infssuzle 12973 |
. . . . . . . . 9
⊢ (((𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0) ∧ (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ))) |
| 115 | 99, 113, 114 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ))) |
| 116 | 115 | ex 412 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝑔(-g‘𝑃)ℎ) ≠ 0 → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ)))) |
| 117 | | imassrn 6089 |
. . . . . . . . . . 11
⊢ (𝐷 “ (𝐼 ∖ { 0 })) ⊆ ran 𝐷 |
| 118 | | frn 6743 |
. . . . . . . . . . . 12
⊢ (𝐷:(Base‘𝑃)⟶ℝ* → ran
𝐷 ⊆
ℝ*) |
| 119 | 28, 118 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran 𝐷 ⊆
ℝ* |
| 120 | 117, 119 | sstri 3993 |
. . . . . . . . . 10
⊢ (𝐷 “ (𝐼 ∖ { 0 })) ⊆
ℝ* |
| 121 | 120, 38 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ ℝ*) |
| 122 | 121 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ ℝ*) |
| 123 | | ringgrp 20235 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
| 124 | 19, 123 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝑃 ∈ Grp) |
| 125 | 124 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑃 ∈ Grp) |
| 126 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝑀) ⊆ 𝐼 |
| 127 | 126, 4 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∩ 𝑀) ⊆ (Base‘𝑃)) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝐼 ∩ 𝑀) ⊆ (Base‘𝑃)) |
| 129 | 128, 89 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ (Base‘𝑃)) |
| 130 | 128, 93 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ (Base‘𝑃)) |
| 131 | 1, 87 | grpsubcl 19038 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Grp ∧ 𝑔 ∈ (Base‘𝑃) ∧ ℎ ∈ (Base‘𝑃)) → (𝑔(-g‘𝑃)ℎ) ∈ (Base‘𝑃)) |
| 132 | 125, 129,
130, 131 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝑔(-g‘𝑃)ℎ) ∈ (Base‘𝑃)) |
| 133 | 10, 11, 1 | deg1xrcl 26121 |
. . . . . . . . 9
⊢ ((𝑔(-g‘𝑃)ℎ) ∈ (Base‘𝑃) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈
ℝ*) |
| 134 | 132, 133 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈
ℝ*) |
| 135 | 122, 134 | xrlenltd 11327 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ)) ↔ ¬ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 136 | 116, 135 | sylibd 239 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝑔(-g‘𝑃)ℎ) ≠ 0 → ¬ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 137 | 136 | necon4ad 2959 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ (𝑔(-g‘𝑃)ℎ) = 0 )) |
| 138 | 98, 137 | syld 47 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ (𝑔(-g‘𝑃)ℎ) = 0 )) |
| 139 | 1, 12, 87 | grpsubeq0 19044 |
. . . . 5
⊢ ((𝑃 ∈ Grp ∧ 𝑔 ∈ (Base‘𝑃) ∧ ℎ ∈ (Base‘𝑃)) → ((𝑔(-g‘𝑃)ℎ) = 0 ↔ 𝑔 = ℎ)) |
| 140 | 125, 129,
130, 139 | syl3anc 1373 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝑔(-g‘𝑃)ℎ) = 0 ↔ 𝑔 = ℎ)) |
| 141 | 138, 140 | sylibd 239 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ 𝑔 = ℎ)) |
| 142 | 141 | ralrimivva 3202 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∀𝑔 ∈ (𝐼 ∩ 𝑀)∀ℎ ∈ (𝐼 ∩ 𝑀)(((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ 𝑔 = ℎ)) |
| 143 | | fveqeq2 6915 |
. . 3
⊢ (𝑔 = ℎ → ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
↔ (𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
| 144 | 143 | reu4 3737 |
. 2
⊢
(∃!𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
↔ (∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
∀𝑔 ∈ (𝐼 ∩ 𝑀)∀ℎ ∈ (𝐼 ∩ 𝑀)(((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ 𝑔 = ℎ))) |
| 145 | 86, 142, 144 | sylanbrc 583 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |