Step | Hyp | Ref
| Expression |
1 | | mplsubg.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | mplsubg.p |
. . 3
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
3 | | mplsubg.u |
. . 3
⊢ 𝑈 = (Base‘𝑃) |
4 | | mplsubg.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
5 | | mpllss.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | | ringgrp 19788 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Grp) |
8 | 1, 2, 3, 4, 7 | mplsubg 21208 |
. 2
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) |
9 | 1, 4, 5 | psrring 21180 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Ring) |
10 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | | eqid 2738 |
. . . . 5
⊢
(1r‘𝑆) = (1r‘𝑆) |
12 | 10, 11 | ringidcl 19807 |
. . . 4
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
13 | 9, 12 | syl 17 |
. . 3
⊢ (𝜑 → (1r‘𝑆) ∈ (Base‘𝑆)) |
14 | | eqid 2738 |
. . . . 5
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
15 | | eqid 2738 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
16 | | eqid 2738 |
. . . . 5
⊢
(1r‘𝑅) = (1r‘𝑅) |
17 | 1, 4, 5, 14, 15, 16, 11 | psr1 21181 |
. . . 4
⊢ (𝜑 → (1r‘𝑆) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))) |
18 | | ovex 7308 |
. . . . . . . 8
⊢
(ℕ0 ↑m 𝐼) ∈ V |
19 | 18 | mptrabex 7101 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V |
20 | | funmpt 6472 |
. . . . . . 7
⊢ Fun
(𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) |
21 | | fvex 6787 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
22 | 19, 20, 21 | 3pm3.2i 1338 |
. . . . . 6
⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∧
(0g‘𝑅)
∈ V) |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∧
(0g‘𝑅)
∈ V)) |
24 | | snfi 8834 |
. . . . . 6
⊢ {(𝐼 × {0})} ∈
Fin |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → {(𝐼 × {0})} ∈ Fin) |
26 | | eldifsni 4723 |
. . . . . . . 8
⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝐼 × {0})}) → 𝑘 ≠ (𝐼 × {0})) |
27 | 26 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝐼 × {0})})) → 𝑘 ≠ (𝐼 × {0})) |
28 | | ifnefalse 4471 |
. . . . . . 7
⊢ (𝑘 ≠ (𝐼 × {0}) → if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ {(𝐼 × {0})})) → if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
30 | 18 | rabex 5256 |
. . . . . . 7
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
32 | 29, 31 | suppss2 8016 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) supp
(0g‘𝑅))
⊆ {(𝐼 ×
{0})}) |
33 | | suppssfifsupp 9143 |
. . . . 5
⊢ ((((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∧
(0g‘𝑅)
∈ V) ∧ ({(𝐼
× {0})} ∈ Fin ∧ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) supp
(0g‘𝑅))
⊆ {(𝐼 × {0})}))
→ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) finSupp
(0g‘𝑅)) |
34 | 23, 25, 32, 33 | syl12anc 834 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑘 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) finSupp
(0g‘𝑅)) |
35 | 17, 34 | eqbrtrd 5096 |
. . 3
⊢ (𝜑 → (1r‘𝑆) finSupp
(0g‘𝑅)) |
36 | 2, 1, 10, 15, 3 | mplelbas 21199 |
. . 3
⊢
((1r‘𝑆) ∈ 𝑈 ↔ ((1r‘𝑆) ∈ (Base‘𝑆) ∧
(1r‘𝑆)
finSupp (0g‘𝑅))) |
37 | 13, 35, 36 | sylanbrc 583 |
. 2
⊢ (𝜑 → (1r‘𝑆) ∈ 𝑈) |
38 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝐼 ∈ 𝑊) |
39 | 5 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑅 ∈ Ring) |
40 | | eqid 2738 |
. . . 4
⊢ (
∘f + “ ((𝑥 supp (0g‘𝑅)) × (𝑦 supp (0g‘𝑅)))) = ( ∘f + “
((𝑥 supp
(0g‘𝑅))
× (𝑦 supp
(0g‘𝑅)))) |
41 | | eqid 2738 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
42 | | simprl 768 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈) |
43 | | simprr 770 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
44 | 1, 2, 3, 38, 39, 14, 15, 40, 41, 42, 43 | mplsubrglem 21210 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑥(.r‘𝑆)𝑦) ∈ 𝑈) |
45 | 44 | ralrimivva 3123 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑥(.r‘𝑆)𝑦) ∈ 𝑈) |
46 | | eqid 2738 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
47 | 10, 11, 46 | issubrg2 20044 |
. . 3
⊢ (𝑆 ∈ Ring → (𝑈 ∈ (SubRing‘𝑆) ↔ (𝑈 ∈ (SubGrp‘𝑆) ∧ (1r‘𝑆) ∈ 𝑈 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑥(.r‘𝑆)𝑦) ∈ 𝑈))) |
48 | 9, 47 | syl 17 |
. 2
⊢ (𝜑 → (𝑈 ∈ (SubRing‘𝑆) ↔ (𝑈 ∈ (SubGrp‘𝑆) ∧ (1r‘𝑆) ∈ 𝑈 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑥(.r‘𝑆)𝑦) ∈ 𝑈))) |
49 | 8, 37, 45, 48 | mpbir3and 1341 |
1
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑆)) |