| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 3 | | ringcmn 20279 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 4 | 3 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CMnd) |
| 5 | 4 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑅 ∈ CMnd) |
| 6 | | ovex 7464 |
. . . . . . . 8
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 7 | 6 | rabex 5339 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V |
| 8 | 7 | rabex 5339 |
. . . . . 6
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ∈ V |
| 9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ∈ V) |
| 10 | | simpll1 1213 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → 𝑅 ∈ Ring) |
| 11 | | psropprmul.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝐼 mPwSer 𝑅) |
| 12 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin} |
| 13 | | psropprmul.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑌) |
| 14 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
| 15 | 11, 1, 12, 13, 14 | psrelbas 21954 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐺:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 17 | | elrabi 3687 |
. . . . . . . 8
⊢ (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} → 𝑒 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
| 18 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐺:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
∧ 𝑒 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐺‘𝑒) ∈ (Base‘𝑅)) |
| 19 | 16, 17, 18 | syl2an 596 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝐺‘𝑒) ∈ (Base‘𝑅)) |
| 20 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
| 21 | 11, 1, 12, 13, 20 | psrelbas 21954 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 22 | 21 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → 𝐹:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 23 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ⊆ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin} |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} = {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} |
| 25 | 12, 24 | psrbagconcl 21947 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝑏 ∘f − 𝑒) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 26 | 25 | adantll 714 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝑏 ∘f − 𝑒) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 27 | 23, 26 | sselid 3981 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝑏 ∘f − 𝑒) ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
| 28 | 22, 27 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝐹‘(𝑏 ∘f − 𝑒)) ∈ (Base‘𝑅)) |
| 29 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 30 | 1, 29 | ringcl 20247 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘𝑒) ∈ (Base‘𝑅) ∧ (𝐹‘(𝑏 ∘f − 𝑒)) ∈ (Base‘𝑅)) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))) ∈ (Base‘𝑅)) |
| 31 | 10, 19, 28, 30 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))) ∈ (Base‘𝑅)) |
| 32 | 31 | fmpttd 7135 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}⟶(Base‘𝑅)) |
| 33 | | mptexg 7241 |
. . . . . . 7
⊢ ({𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ∈ V → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∈ V) |
| 34 | 8, 33 | mp1i 13 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∈ V) |
| 35 | | funmpt 6604 |
. . . . . . 7
⊢ Fun
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) |
| 36 | 35 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → Fun
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))))) |
| 37 | | fvexd 6921 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(0g‘𝑅)
∈ V) |
| 38 | 12 | psrbaglefi 21946 |
. . . . . . 7
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ∈ Fin) |
| 39 | 38 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ∈ Fin) |
| 40 | | suppssdm 8202 |
. . . . . . . 8
⊢ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) supp
(0g‘𝑅))
⊆ dom (𝑒 ∈
{𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) |
| 41 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) = (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) |
| 42 | 41 | dmmptss 6261 |
. . . . . . . 8
⊢ dom
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} |
| 43 | 40, 42 | sstri 3993 |
. . . . . . 7
⊢ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} |
| 44 | 43 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 45 | | suppssfifsupp 9420 |
. . . . . 6
⊢ ((((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∈ V ∧ Fun (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∧
(0g‘𝑅)
∈ V) ∧ ({𝑑 ∈
{𝑎 ∈
(ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ∈ Fin ∧ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏})) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) finSupp
(0g‘𝑅)) |
| 46 | 34, 36, 37, 39, 44, 45 | syl32anc 1380 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) finSupp
(0g‘𝑅)) |
| 47 | 12, 24 | psrbagconf1o 21949 |
. . . . . 6
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐)):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}–1-1-onto→{𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 48 | 47 | adantl 481 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐)):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}–1-1-onto→{𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 49 | 1, 2, 5, 9, 32, 46, 48 | gsumf1o 19934 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))))) = (𝑅 Σg ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐))))) |
| 50 | 12, 24 | psrbagconcl 21947 |
. . . . . . . 8
⊢ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝑏 ∘f − 𝑐) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 51 | 50 | adantll 714 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝑏 ∘f − 𝑐) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) |
| 52 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐)) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐))) |
| 53 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) = (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))))) |
| 54 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑒 = (𝑏 ∘f − 𝑐) → (𝐺‘𝑒) = (𝐺‘(𝑏 ∘f − 𝑐))) |
| 55 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑒 = (𝑏 ∘f − 𝑐) → (𝑏 ∘f − 𝑒) = (𝑏 ∘f − (𝑏 ∘f −
𝑐))) |
| 56 | 55 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑒 = (𝑏 ∘f − 𝑐) → (𝐹‘(𝑏 ∘f − 𝑒)) = (𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐)))) |
| 57 | 54, 56 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑒 = (𝑏 ∘f − 𝑐) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))) = ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐))))) |
| 58 | 51, 52, 53, 57 | fmptco 7149 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐)))))) |
| 59 | | reldmpsr 21934 |
. . . . . . . . . . . . . 14
⊢ Rel dom
mPwSer |
| 60 | 11, 13, 59 | strov2rcl 17255 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ 𝐵 → 𝐼 ∈ V) |
| 61 | 60 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐼 ∈ V) |
| 62 | 61 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → 𝐼 ∈ V) |
| 63 | 12 | psrbagf 21938 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} → 𝑏:𝐼⟶ℕ0) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑏:𝐼⟶ℕ0) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → 𝑏:𝐼⟶ℕ0) |
| 66 | | elrabi 3687 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
| 67 | 12 | psrbagf 21938 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} → 𝑐:𝐼⟶ℕ0) |
| 68 | 66, 67 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} → 𝑐:𝐼⟶ℕ0) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → 𝑐:𝐼⟶ℕ0) |
| 70 | | nn0cn 12536 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ ℕ0
→ 𝑒 ∈
ℂ) |
| 71 | | nn0cn 12536 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ℕ0
→ 𝑓 ∈
ℂ) |
| 72 | | nncan 11538 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ ℂ ∧ 𝑓 ∈ ℂ) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
| 73 | 70, 71, 72 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑒 ∈ ℕ0
∧ 𝑓 ∈
ℕ0) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
| 74 | 73 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ Ring
∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) ∧ (𝑒 ∈ ℕ0 ∧ 𝑓 ∈ ℕ0))
→ (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
| 75 | 62, 65, 69, 74 | caonncan 7741 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝑏 ∘f − (𝑏 ∘f −
𝑐)) = 𝑐) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → (𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐))) = (𝐹‘𝑐)) |
| 77 | 76 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐)))) = ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘𝑐))) |
| 78 | | psropprmul.s |
. . . . . . . . 9
⊢ 𝑆 =
(oppr‘𝑅) |
| 79 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 80 | 1, 29, 78, 79 | opprmul 20337 |
. . . . . . . 8
⊢ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))) = ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘𝑐)) |
| 81 | 77, 80 | eqtr4di 2795 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏}) → ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐)))) = ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))) |
| 82 | 81 | mpteq2dva 5242 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘(𝑏 ∘f − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘f − (𝑏 ∘f −
𝑐))))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))) |
| 83 | 58, 82 | eqtrd 2777 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))) |
| 84 | 83 | oveq2d 7447 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ (𝑏 ∘f − 𝑐)))) = (𝑅 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))))) |
| 85 | 8 | mptex 7243 |
. . . . . . . 8
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))) ∈ V |
| 86 | 85 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))) ∈ V) |
| 87 | | id 22 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
| 88 | 78 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑆 ∈ V |
| 89 | 88 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑆 ∈ V) |
| 90 | 78, 1 | opprbas 20341 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑆) |
| 91 | 90 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘𝑆)) |
| 92 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 93 | 78, 92 | oppradd 20343 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑆) |
| 94 | 93 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(+g‘𝑅) =
(+g‘𝑆)) |
| 95 | 86, 87, 89, 91, 94 | gsumpropd 18691 |
. . . . . 6
⊢ (𝑅 ∈ Ring → (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))))) |
| 96 | 95 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))))) |
| 97 | 96 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))))) |
| 98 | 49, 84, 97 | 3eqtrd 2781 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐)))))) |
| 99 | 98 | mpteq2dva 5242 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒)))))) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))))) |
| 100 | | psropprmul.t |
. . 3
⊢ · =
(.r‘𝑌) |
| 101 | 11, 13, 29, 100, 12, 14, 20 | psrmulfval 21963 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐺 · 𝐹) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘f − 𝑒))))))) |
| 102 | | psropprmul.z |
. . 3
⊢ 𝑍 = (𝐼 mPwSer 𝑆) |
| 103 | | eqid 2737 |
. . 3
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 104 | | psropprmul.u |
. . 3
⊢ ∙ =
(.r‘𝑍) |
| 105 | 90 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (Base‘𝑅) = (Base‘𝑆)) |
| 106 | 105 | psrbaspropd 22236 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) |
| 107 | 11 | fveq2i 6909 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘(𝐼 mPwSer 𝑅)) |
| 108 | 13, 107 | eqtri 2765 |
. . . . 5
⊢ 𝐵 = (Base‘(𝐼 mPwSer 𝑅)) |
| 109 | 102 | fveq2i 6909 |
. . . . 5
⊢
(Base‘𝑍) =
(Base‘(𝐼 mPwSer 𝑆)) |
| 110 | 106, 108,
109 | 3eqtr4g 2802 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐵 = (Base‘𝑍)) |
| 111 | 20, 110 | eleqtrd 2843 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ (Base‘𝑍)) |
| 112 | 14, 110 | eleqtrd 2843 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (Base‘𝑍)) |
| 113 | 102, 103,
79, 104, 12, 111, 112 | psrmulfval 21963 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘f − 𝑐))))))) |
| 114 | 99, 101, 113 | 3eqtr4rd 2788 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) |