Step | Hyp | Ref
| Expression |
1 | | ig1pval.g |
. . . 4
⊢ 𝐺 =
(idlGen1p‘𝑅) |
2 | | elex 3447 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
3 | | fveq2 6766 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
4 | | ig1pval.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
5 | 3, 4 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
6 | 5 | fveq2d 6770 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(LIdeal‘(Poly1‘𝑟)) = (LIdeal‘𝑃)) |
7 | | ig1pval.u |
. . . . . . . 8
⊢ 𝑈 = (LIdeal‘𝑃) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
(LIdeal‘(Poly1‘𝑟)) = 𝑈) |
9 | 5 | fveq2d 6770 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = (0g‘𝑃)) |
10 | | ig1pval.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑃) |
11 | 9, 10 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = 0 ) |
12 | 11 | sneqd 4573 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
{(0g‘(Poly1‘𝑟))} = { 0 }) |
13 | 12 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑖 =
{(0g‘(Poly1‘𝑟))} ↔ 𝑖 = { 0 })) |
14 | | fveq2 6766 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (Monic1p‘𝑟) =
(Monic1p‘𝑅)) |
15 | | ig1pval.m |
. . . . . . . . . . 11
⊢ 𝑀 =
(Monic1p‘𝑅) |
16 | 14, 15 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Monic1p‘𝑟) = 𝑀) |
17 | 16 | ineq2d 4146 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑖 ∩ (Monic1p‘𝑟)) = (𝑖 ∩ 𝑀)) |
18 | | fveq2 6766 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
19 | | ig1pval.d |
. . . . . . . . . . . 12
⊢ 𝐷 = ( deg1
‘𝑅) |
20 | 18, 19 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = 𝐷) |
21 | 20 | fveq1d 6768 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟)‘𝑔) = (𝐷‘𝑔)) |
22 | 12 | difeq2d 4056 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (𝑖 ∖
{(0g‘(Poly1‘𝑟))}) = (𝑖 ∖ { 0 })) |
23 | 20, 22 | imaeq12d 5963 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})) = (𝐷 “ (𝑖 ∖ { 0 }))) |
24 | 23 | infeq1d 9223 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → inf((( deg1 ‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
)) |
25 | 21, 24 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ((( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ) ↔ (𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))) |
26 | 17, 25 | riotaeqbidv 7227 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < )) =
(℩𝑔 ∈
(𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))) |
27 | 13, 11, 26 | ifbieq12d 4487 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → if(𝑖 =
{(0g‘(Poly1‘𝑟))},
(0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ))) = if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
)))) |
28 | 8, 27 | mpteq12dv 5164 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑖 ∈
(LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 =
{(0g‘(Poly1‘𝑟))},
(0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < )))) = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
29 | | df-ig1p 25309 |
. . . . . 6
⊢
idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈
(LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 =
{(0g‘(Poly1‘𝑟))},
(0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ))))) |
30 | 28, 29, 7 | mptfvmpt 7096 |
. . . . 5
⊢ (𝑅 ∈ V →
(idlGen1p‘𝑅) = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
31 | 2, 30 | syl 17 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (idlGen1p‘𝑅) = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
32 | 1, 31 | eqtrid 2790 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝐺 = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
33 | 32 | fveq1d 6768 |
. 2
⊢ (𝑅 ∈ 𝑉 → (𝐺‘𝐼) = ((𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))‘𝐼)) |
34 | | eqeq1 2742 |
. . . 4
⊢ (𝑖 = 𝐼 → (𝑖 = { 0 } ↔ 𝐼 = { 0 })) |
35 | | ineq1 4139 |
. . . . 5
⊢ (𝑖 = 𝐼 → (𝑖 ∩ 𝑀) = (𝐼 ∩ 𝑀)) |
36 | | difeq1 4049 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (𝑖 ∖ { 0 }) = (𝐼 ∖ { 0 })) |
37 | 36 | imaeq2d 5962 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (𝐷 “ (𝑖 ∖ { 0 })) = (𝐷 “ (𝐼 ∖ { 0 }))) |
38 | 37 | infeq1d 9223 |
. . . . . 6
⊢ (𝑖 = 𝐼 → inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < ) =
inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
39 | 38 | eqeq2d 2749 |
. . . . 5
⊢ (𝑖 = 𝐼 → ((𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < )
↔ (𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
40 | 35, 39 | riotaeqbidv 7227 |
. . . 4
⊢ (𝑖 = 𝐼 → (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < )) =
(℩𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
41 | 34, 40 | ifbieq2d 4485 |
. . 3
⊢ (𝑖 = 𝐼 → if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < ))) =
if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)))) |
42 | | eqid 2738 |
. . 3
⊢ (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < )))) =
(𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
)))) |
43 | 10 | fvexi 6780 |
. . . 4
⊢ 0 ∈
V |
44 | | riotaex 7228 |
. . . 4
⊢
(℩𝑔
∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
∈ V |
45 | 43, 44 | ifex 4509 |
. . 3
⊢ if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
∈ V |
46 | 41, 42, 45 | fvmpt 6867 |
. 2
⊢ (𝐼 ∈ 𝑈 → ((𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)))) |
47 | 33, 46 | sylan9eq 2798 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)))) |