Step | Hyp | Ref
| Expression |
1 | | ig1pval.g |
. . . 4
⊢ 𝐺 =
(idlGen1p‘𝑅) |
2 | | elex 3429 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
3 | | fveq2 6433 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
4 | | ig1pval.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
5 | 3, 4 | syl6eqr 2879 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = 𝑃) |
6 | 5 | fveq2d 6437 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(LIdeal‘(Poly1‘𝑟)) = (LIdeal‘𝑃)) |
7 | | ig1pval.u |
. . . . . . . 8
⊢ 𝑈 = (LIdeal‘𝑃) |
8 | 6, 7 | syl6eqr 2879 |
. . . . . . 7
⊢ (𝑟 = 𝑅 →
(LIdeal‘(Poly1‘𝑟)) = 𝑈) |
9 | 5 | fveq2d 6437 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = (0g‘𝑃)) |
10 | | ig1pval.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑃) |
11 | 9, 10 | syl6eqr 2879 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 →
(0g‘(Poly1‘𝑟)) = 0 ) |
12 | 11 | sneqd 4409 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
{(0g‘(Poly1‘𝑟))} = { 0 }) |
13 | 12 | eqeq2d 2835 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑖 =
{(0g‘(Poly1‘𝑟))} ↔ 𝑖 = { 0 })) |
14 | | fveq2 6433 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (Monic1p‘𝑟) =
(Monic1p‘𝑅)) |
15 | | ig1pval.m |
. . . . . . . . . . 11
⊢ 𝑀 =
(Monic1p‘𝑅) |
16 | 14, 15 | syl6eqr 2879 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Monic1p‘𝑟) = 𝑀) |
17 | 16 | ineq2d 4041 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (𝑖 ∩ (Monic1p‘𝑟)) = (𝑖 ∩ 𝑀)) |
18 | | fveq2 6433 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = ( deg1
‘𝑅)) |
19 | | ig1pval.d |
. . . . . . . . . . . 12
⊢ 𝐷 = ( deg1
‘𝑅) |
20 | 18, 19 | syl6eqr 2879 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → ( deg1 ‘𝑟) = 𝐷) |
21 | 20 | fveq1d 6435 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟)‘𝑔) = (𝐷‘𝑔)) |
22 | 12 | difeq2d 3955 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (𝑖 ∖
{(0g‘(Poly1‘𝑟))}) = (𝑖 ∖ { 0 })) |
23 | 20, 22 | imaeq12d 5708 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (( deg1 ‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})) = (𝐷 “ (𝑖 ∖ { 0 }))) |
24 | 23 | infeq1d 8652 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → inf((( deg1 ‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
)) |
25 | 21, 24 | eqeq12d 2840 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → ((( deg1 ‘𝑟)‘𝑔) = inf((( deg1 ‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ) ↔ (𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))) |
26 | 17, 25 | riotaeqbidv 6869 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < )) =
(℩𝑔 ∈
(𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))) |
27 | 13, 11, 26 | ifbieq12d 4333 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → if(𝑖 =
{(0g‘(Poly1‘𝑟))},
(0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ))) = if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
)))) |
28 | 8, 27 | mpteq12dv 4956 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑖 ∈
(LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 =
{(0g‘(Poly1‘𝑟))},
(0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < )))) = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
29 | | df-ig1p 24293 |
. . . . . 6
⊢
idlGen1p = (𝑟 ∈ V ↦ (𝑖 ∈
(LIdeal‘(Poly1‘𝑟)) ↦ if(𝑖 =
{(0g‘(Poly1‘𝑟))},
(0g‘(Poly1‘𝑟)), (℩𝑔 ∈ (𝑖 ∩ (Monic1p‘𝑟))(( deg1
‘𝑟)‘𝑔) = inf((( deg1
‘𝑟) “ (𝑖 ∖
{(0g‘(Poly1‘𝑟))})), ℝ, < ))))) |
30 | 28, 29, 7 | mptfvmpt 6746 |
. . . . 5
⊢ (𝑅 ∈ V →
(idlGen1p‘𝑅) = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
31 | 2, 30 | syl 17 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (idlGen1p‘𝑅) = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
32 | 1, 31 | syl5eq 2873 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝐺 = (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))) |
33 | 32 | fveq1d 6435 |
. 2
⊢ (𝑅 ∈ 𝑉 → (𝐺‘𝐼) = ((𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))‘𝐼)) |
34 | | eqeq1 2829 |
. . . 4
⊢ (𝑖 = 𝐼 → (𝑖 = { 0 } ↔ 𝐼 = { 0 })) |
35 | | ineq1 4034 |
. . . . 5
⊢ (𝑖 = 𝐼 → (𝑖 ∩ 𝑀) = (𝐼 ∩ 𝑀)) |
36 | | difeq1 3948 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (𝑖 ∖ { 0 }) = (𝐼 ∖ { 0 })) |
37 | 36 | imaeq2d 5707 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (𝐷 “ (𝑖 ∖ { 0 })) = (𝐷 “ (𝐼 ∖ { 0 }))) |
38 | 37 | infeq1d 8652 |
. . . . . 6
⊢ (𝑖 = 𝐼 → inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < ) =
inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)) |
39 | 38 | eqeq2d 2835 |
. . . . 5
⊢ (𝑖 = 𝐼 → ((𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < )
↔ (𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
40 | 35, 39 | riotaeqbidv 6869 |
. . . 4
⊢ (𝑖 = 𝐼 → (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < )) =
(℩𝑔 ∈
(𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
))) |
41 | 34, 40 | ifbieq2d 4331 |
. . 3
⊢ (𝑖 = 𝐼 → if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < ))) =
if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)))) |
42 | | eqid 2825 |
. . 3
⊢ (𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, < )))) =
(𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
)))) |
43 | 10 | fvexi 6447 |
. . . 4
⊢ 0 ∈
V |
44 | | riotaex 6870 |
. . . 4
⊢
(℩𝑔
∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < ))
∈ V |
45 | 43, 44 | ifex 4354 |
. . 3
⊢ if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, < )))
∈ V |
46 | 41, 42, 45 | fvmpt 6529 |
. 2
⊢ (𝐼 ∈ 𝑈 → ((𝑖 ∈ 𝑈 ↦ if(𝑖 = { 0 }, 0 , (℩𝑔 ∈ (𝑖 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝑖 ∖ { 0 })), ℝ, <
))))‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)))) |
47 | 33, 46 | sylan9eq 2881 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈) → (𝐺‘𝐼) = if(𝐼 = { 0 }, 0 , (℩𝑔 ∈ (𝐼 ∩ 𝑀)(𝐷‘𝑔) = inf((𝐷 “ (𝐼 ∖ { 0 })), ℝ, <
)))) |