Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
2 | | ig1peu.u |
. . . . . . . . . . 11
⊢ 𝑈 = (LIdeal‘𝑃) |
3 | 1, 2 | lidlss 19031 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑈 → 𝐼 ⊆ (Base‘𝑃)) |
4 | 3 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐼 ⊆ (Base‘𝑃)) |
5 | 4 | ssdifd 3708 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ⊆
((Base‘𝑃) ∖ {
0
})) |
6 | | imass2 5420 |
. . . . . . . 8
⊢ ((𝐼 ∖ { 0 }) ⊆
((Base‘𝑃) ∖ {
0 })
→ (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (𝐷 “ ((Base‘𝑃) ∖ { 0 }))) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆ (𝐷 “ ((Base‘𝑃) ∖ { 0 }))) |
8 | | drngring 18577 |
. . . . . . . . 9
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
9 | 8 | 3ad2ant1 1075 |
. . . . . . . 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 23653 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (𝐷 “ ((Base‘𝑃) ∖ { 0 })) ⊆
ℕ0) |
14 | 9, 13 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ ((Base‘𝑃) ∖ { 0 })) ⊆
ℕ0) |
15 | 7, 14 | sstrd 3578 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆
ℕ0) |
16 | | nn0uz 11598 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
17 | 15, 16 | syl6sseq 3614 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0)) |
18 | 11 | ply1ring 19439 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
19 | 9, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝑃 ∈ Ring) |
20 | | simp2 1055 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐼 ∈ 𝑈) |
21 | 2, 12 | lidl0cl 19033 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 0 ∈ 𝐼) |
22 | 19, 20, 21 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 0 ∈ 𝐼) |
23 | 22 | snssd 4281 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → { 0 } ⊆
𝐼) |
24 | | simp3 1056 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝐼 ≠ { 0 }) |
25 | 24 | necomd 2837 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → { 0 } ≠ 𝐼) |
26 | | pssdifn0 3898 |
. . . . . . 7
⊢ (({ 0 } ⊆
𝐼 ∧ { 0 } ≠ 𝐼) → (𝐼 ∖ { 0 }) ≠
∅) |
27 | 23, 25, 26 | syl2anc 691 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ≠
∅) |
28 | 10, 11, 1 | deg1xrf 23645 |
. . . . . . . . . 10
⊢ 𝐷:(Base‘𝑃)⟶ℝ* |
29 | | ffn 5958 |
. . . . . . . . . 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 3710 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) |
33 | | fnimaeq0 5926 |
. . . . . . . 8
⊢ ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) →
((𝐷 “ (𝐼 ∖ { 0 })) = ∅ ↔
(𝐼 ∖ { 0 }) =
∅)) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐷 “ (𝐼 ∖ { 0 })) = ∅ ↔
(𝐼 ∖ { 0 }) =
∅)) |
35 | 34 | necon3bid 2826 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ((𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅ ↔
(𝐼 ∖ { 0 }) ≠
∅)) |
36 | 27, 35 | mpbird 246 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐷 “ (𝐼 ∖ { 0 })) ≠
∅) |
37 | | infssuzcl 11648 |
. . . . 5
⊢ (((𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0) ∧ (𝐷 “ (𝐼 ∖ { 0 })) ≠ ∅) →
inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
38 | 17, 36, 37 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
39 | | fvelimab 6163 |
. . . . 5
⊢ ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) →
(inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 })) ↔ ∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
40 | 31, 32, 39 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ (𝐷 “ (𝐼 ∖ { 0 })) ↔ ∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
41 | 38, 40 | mpbid 221 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
42 | 19 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝑃 ∈ Ring) |
43 | | simpl2 1058 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝐼 ∈ 𝑈) |
44 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝑅 ∈ Ring) |
45 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
46 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
47 | 11, 45, 46, 1 | ply1sclf 19476 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃)) |
48 | 44, 47 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃)) |
49 | | simpl1 1057 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → 𝑅 ∈
DivRing) |
50 | 32 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ∈ (Base‘𝑃)) |
51 | | eldifsni 4261 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ (𝐼 ∖ { 0 }) → ℎ ≠ 0 ) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ≠ 0 ) |
53 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
54 | 11, 1, 12, 53 | drnguc1p 23734 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ DivRing ∧ ℎ ∈ (Base‘𝑃) ∧ ℎ ≠ 0 ) → ℎ ∈
(Unic1p‘𝑅)) |
55 | 49, 50, 52, 54 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ∈
(Unic1p‘𝑅)) |
56 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
57 | 10, 56, 53 | uc1pldg 23712 |
. . . . . . . . . . . 12
⊢ (ℎ ∈
(Unic1p‘𝑅)
→ ((coe1‘ℎ)‘(𝐷‘ℎ)) ∈ (Unit‘𝑅)) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((coe1‘ℎ)‘(𝐷‘ℎ)) ∈ (Unit‘𝑅)) |
59 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(invr‘𝑅) = (invr‘𝑅) |
60 | 56, 59 | unitinvcl 18497 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
((coe1‘ℎ)‘(𝐷‘ℎ)) ∈ (Unit‘𝑅)) → ((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Unit‘𝑅)) |
61 | 44, 58, 60 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Unit‘𝑅)) |
62 | 46, 56 | unitcl 18482 |
. . . . . . . . . 10
⊢
(((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Unit‘𝑅) → ((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Base‘𝑅)) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (Base‘𝑅)) |
64 | 48, 63 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ)))) ∈ (Base‘𝑃)) |
65 | | eldifi 3694 |
. . . . . . . . 9
⊢ (ℎ ∈ (𝐼 ∖ { 0 }) → ℎ ∈ 𝐼) |
66 | 65 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ℎ ∈ 𝐼) |
67 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑃) = (.r‘𝑃) |
68 | 2, 1, 67 | lidlmcl 19038 |
. . . . . . . 8
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ)))) ∈ (Base‘𝑃) ∧ ℎ ∈ 𝐼)) → (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝐼) |
69 | 42, 43, 64, 66, 68 | syl22anc 1319 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝐼) |
70 | | ig1peu.m |
. . . . . . . . 9
⊢ 𝑀 =
(Monic1p‘𝑅) |
71 | 53, 70, 11, 67, 45, 10, 59 | uc1pmon1p 23715 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ ℎ ∈
(Unic1p‘𝑅)) → (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝑀) |
72 | 44, 55, 71 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ 𝑀) |
73 | 69, 72 | elind 3760 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ (𝐼 ∩ 𝑀)) |
74 | | eqid 2610 |
. . . . . . . . . 10
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) |
75 | 74, 56 | unitrrg 19114 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
76 | 44, 75 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
(Unit‘𝑅) ⊆
(RLReg‘𝑅)) |
77 | 76, 61 | sseldd 3569 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) →
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (RLReg‘𝑅)) |
78 | 10, 11, 74, 1, 67, 45 | deg1mul3 23679 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))) ∈ (RLReg‘𝑅) ∧ ℎ ∈ (Base‘𝑃)) → (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ)) |
79 | 44, 77, 50, 78 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ)) |
80 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑔 = (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) → (𝐷‘𝑔) = (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ))) |
81 | 80 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑔 = (((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) → ((𝐷‘𝑔) = (𝐷‘ℎ) ↔ (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ))) |
82 | 81 | rspcev 3282 |
. . . . . 6
⊢
(((((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ) ∈ (𝐼 ∩ 𝑀) ∧ (𝐷‘(((algSc‘𝑃)‘((invr‘𝑅)‘((coe1‘ℎ)‘(𝐷‘ℎ))))(.r‘𝑃)ℎ)) = (𝐷‘ℎ)) → ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = (𝐷‘ℎ)) |
83 | 73, 79, 82 | syl2anc 691 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = (𝐷‘ℎ)) |
84 | | eqeq2 2621 |
. . . . . 6
⊢ ((𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ ((𝐷‘𝑔) = (𝐷‘ℎ) ↔ (𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
85 | 84 | rexbidv 3034 |
. . . . 5
⊢ ((𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ (∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = (𝐷‘ℎ) ↔ ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
86 | 83, 85 | syl5ibcom 234 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ ℎ ∈ (𝐼 ∖ { 0 })) → ((𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ ∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
87 | 86 | rexlimdva 3013 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (∃ℎ ∈ (𝐼 ∖ { 0 })(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ ∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
88 | 41, 87 | mpd 15 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
89 | | eqid 2610 |
. . . . . . 7
⊢
(-g‘𝑃) = (-g‘𝑃) |
90 | 9 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ 𝑅 ∈
Ring) |
91 | | inss2 3796 |
. . . . . . . . 9
⊢ (𝐼 ∩ 𝑀) ⊆ 𝑀 |
92 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ (𝐼 ∩ 𝑀)) |
93 | 91, 92 | sseldi 3566 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ 𝑀) |
94 | 93 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ 𝑔 ∈ 𝑀) |
95 | | simprl 790 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ (𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
96 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ (𝐼 ∩ 𝑀)) |
97 | 91, 96 | sseldi 3566 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ 𝑀) |
98 | 97 | adantr 480 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ ℎ ∈ 𝑀) |
99 | | simprr 792 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ (𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
100 | 10, 70, 11, 89, 90, 94, 95, 98, 99 | deg1submon1p 23716 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
→ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
101 | 100 | ex 449 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
102 | 17 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0)) |
103 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → 𝐷 Fn (Base‘𝑃)) |
104 | 32 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃)) |
105 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑃 ∈ Ring) |
106 | | simpl2 1058 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝐼 ∈ 𝑈) |
107 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∩ 𝑀) ⊆ 𝐼 |
108 | 107, 92 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ 𝐼) |
109 | 107, 96 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ 𝐼) |
110 | 2, 89 | lidlsubcl 19037 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑔 ∈ 𝐼 ∧ ℎ ∈ 𝐼)) → (𝑔(-g‘𝑃)ℎ) ∈ 𝐼) |
111 | 105, 106,
108, 109, 110 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝑔(-g‘𝑃)ℎ) ∈ 𝐼) |
112 | 111 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝑔(-g‘𝑃)ℎ) ∈ 𝐼) |
113 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝑔(-g‘𝑃)ℎ) ≠ 0 ) |
114 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ ((𝑔(-g‘𝑃)ℎ) ∈ (𝐼 ∖ { 0 }) ↔ ((𝑔(-g‘𝑃)ℎ) ∈ 𝐼 ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 )) |
115 | 112, 113,
114 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝑔(-g‘𝑃)ℎ) ∈ (𝐼 ∖ { 0 })) |
116 | | fnfvima 6400 |
. . . . . . . . . 10
⊢ ((𝐷 Fn (Base‘𝑃) ∧ (𝐼 ∖ { 0 }) ⊆
(Base‘𝑃) ∧ (𝑔(-g‘𝑃)ℎ) ∈ (𝐼 ∖ { 0 })) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
117 | 103, 104,
115, 116 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) |
118 | | infssuzle 11647 |
. . . . . . . . 9
⊢ (((𝐷 “ (𝐼 ∖ { 0 })) ⊆
(ℤ≥‘0) ∧ (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ (𝐷 “ (𝐼 ∖ { 0 }))) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ))) |
119 | 102, 117,
118 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) ∧ (𝑔(-g‘𝑃)ℎ) ≠ 0 ) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ))) |
120 | 119 | ex 449 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝑔(-g‘𝑃)ℎ) ≠ 0 → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ)))) |
121 | | imassrn 5396 |
. . . . . . . . . . 11
⊢ (𝐷 “ (𝐼 ∖ { 0 })) ⊆ ran 𝐷 |
122 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝐷:(Base‘𝑃)⟶ℝ* → ran
𝐷 ⊆
ℝ*) |
123 | 28, 122 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran 𝐷 ⊆
ℝ* |
124 | 121, 123 | sstri 3577 |
. . . . . . . . . 10
⊢ (𝐷 “ (𝐼 ∖ { 0 })) ⊆
ℝ* |
125 | 124, 38 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ ℝ*) |
126 | 125 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
∈ ℝ*) |
127 | | ringgrp 18375 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
128 | 19, 127 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → 𝑃 ∈ Grp) |
129 | 128 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑃 ∈ Grp) |
130 | 107, 4 | syl5ss 3579 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → (𝐼 ∩ 𝑀) ⊆ (Base‘𝑃)) |
131 | 130 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝐼 ∩ 𝑀) ⊆ (Base‘𝑃)) |
132 | 131, 92 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → 𝑔 ∈ (Base‘𝑃)) |
133 | 131, 96 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ℎ ∈ (Base‘𝑃)) |
134 | 1, 89 | grpsubcl 17318 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Grp ∧ 𝑔 ∈ (Base‘𝑃) ∧ ℎ ∈ (Base‘𝑃)) → (𝑔(-g‘𝑃)ℎ) ∈ (Base‘𝑃)) |
135 | 129, 132,
133, 134 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝑔(-g‘𝑃)ℎ) ∈ (Base‘𝑃)) |
136 | 10, 11, 1 | deg1xrcl 23646 |
. . . . . . . . 9
⊢ ((𝑔(-g‘𝑃)ℎ) ∈ (Base‘𝑃) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈
ℝ*) |
137 | 135, 136 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈
ℝ*) |
138 | | xrlenlt 9982 |
. . . . . . . 8
⊢
((inf((𝐷 “
(𝐼 ∖ { 0 })), ℝ,
< ) ∈ ℝ* ∧ (𝐷‘(𝑔(-g‘𝑃)ℎ)) ∈ ℝ*) →
(inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ)) ↔ ¬ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
139 | 126, 137,
138 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ≤
(𝐷‘(𝑔(-g‘𝑃)ℎ)) ↔ ¬ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
140 | 120, 139 | sylibd 228 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝑔(-g‘𝑃)ℎ) ≠ 0 → ¬ (𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
141 | 140 | necon4ad 2801 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝐷‘(𝑔(-g‘𝑃)ℎ)) < inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
→ (𝑔(-g‘𝑃)ℎ) = 0 )) |
142 | 101, 141 | syld 46 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ (𝑔(-g‘𝑃)ℎ) = 0 )) |
143 | 1, 12, 89 | grpsubeq0 17324 |
. . . . 5
⊢ ((𝑃 ∈ Grp ∧ 𝑔 ∈ (Base‘𝑃) ∧ ℎ ∈ (Base‘𝑃)) → ((𝑔(-g‘𝑃)ℎ) = 0 ↔ 𝑔 = ℎ)) |
144 | 129, 132,
133, 143 | syl3anc 1318 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → ((𝑔(-g‘𝑃)ℎ) = 0 ↔ 𝑔 = ℎ)) |
145 | 142, 144 | sylibd 228 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) ∧ (𝑔 ∈ (𝐼 ∩ 𝑀) ∧ ℎ ∈ (𝐼 ∩ 𝑀))) → (((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ 𝑔 = ℎ)) |
146 | 145 | ralrimivva 2954 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∀𝑔 ∈ (𝐼 ∩ 𝑀)∀ℎ ∈ (𝐼 ∩ 𝑀)(((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ 𝑔 = ℎ)) |
147 | | fveq2 6103 |
. . . 4
⊢ (𝑔 = ℎ → (𝐷‘𝑔) = (𝐷‘ℎ)) |
148 | 147 | eqeq1d 2612 |
. . 3
⊢ (𝑔 = ℎ → ((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
↔ (𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
149 | 148 | reu4 3367 |
. 2
⊢
(∃!𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )
↔ (∃𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
∀𝑔 ∈ (𝐼 ∩ 𝑀)∀ℎ ∈ (𝐼 ∩ 𝑀)(((𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ) ∧
(𝐷‘ℎ) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
→ 𝑔 = ℎ))) |
150 | 88, 146, 149 | sylanbrc 695 |
1
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 }) → ∃!𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |