Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | ringcmn 18404 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
4 | 3 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CMnd) |
5 | 4 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑅 ∈ CMnd) |
6 | | ovex 6577 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
7 | 6 | rabex 4740 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V |
8 | 7 | rabex 4740 |
. . . . . 6
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
V |
9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
V) |
10 | | simpll1 1093 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑅 ∈ Ring) |
11 | | psropprmul.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝐼 mPwSer 𝑅) |
12 | | eqid 2610 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
13 | | psropprmul.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑌) |
14 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
15 | 11, 1, 12, 13, 14 | psrelbas 19200 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
17 | | elrabi 3328 |
. . . . . . . 8
⊢ (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} → 𝑒 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
18 | | ffvelrn 6265 |
. . . . . . . 8
⊢ ((𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
∧ 𝑒 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐺‘𝑒) ∈ (Base‘𝑅)) |
19 | 16, 17, 18 | syl2an 493 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝐺‘𝑒) ∈ (Base‘𝑅)) |
20 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
21 | 11, 1, 12, 13, 20 | psrelbas 19200 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
22 | 21 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
23 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ⊆ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
24 | | reldmpsr 19182 |
. . . . . . . . . . . . 13
⊢ Rel dom
mPwSer |
25 | 11, 13, 24 | strov2rcl 15750 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ 𝐵 → 𝐼 ∈ V) |
26 | 25 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐼 ∈ V) |
27 | 26 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝐼 ∈ V) |
28 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
29 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
30 | | eqid 2610 |
. . . . . . . . . . 11
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} = {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} |
31 | 12, 30 | psrbagconcl 19194 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑒) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
32 | 27, 28, 29, 31 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑒) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
33 | 23, 32 | sseldi 3566 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑒) ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
34 | 22, 33 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝐹‘(𝑏 ∘𝑓 − 𝑒)) ∈ (Base‘𝑅)) |
35 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
36 | 1, 35 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘𝑒) ∈ (Base‘𝑅) ∧ (𝐹‘(𝑏 ∘𝑓 − 𝑒)) ∈ (Base‘𝑅)) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))) ∈ (Base‘𝑅)) |
37 | 10, 19, 34, 36 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))) ∈ (Base‘𝑅)) |
38 | | eqid 2610 |
. . . . . 6
⊢ (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) = (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) |
39 | 37, 38 | fmptd 6292 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}⟶(Base‘𝑅)) |
40 | | mptexg 6389 |
. . . . . . 7
⊢ ({𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈ V →
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∈ V) |
41 | 8, 40 | mp1i 13 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∈ V) |
42 | | funmpt 5840 |
. . . . . . 7
⊢ Fun
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) |
43 | 42 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → Fun
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) |
44 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(0g‘𝑅)
∈ V) |
46 | 12 | psrbaglefi 19193 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
Fin) |
47 | 26, 46 | sylan 487 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
Fin) |
48 | | suppssdm 7195 |
. . . . . . . 8
⊢ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ dom (𝑒 ∈
{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) |
49 | 38 | dmmptss 5548 |
. . . . . . . 8
⊢ dom
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} |
50 | 48, 49 | sstri 3577 |
. . . . . . 7
⊢ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} |
51 | 50 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
52 | | suppssfifsupp 8173 |
. . . . . 6
⊢ ((((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∈ V ∧ Fun (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∧
(0g‘𝑅)
∈ V) ∧ ({𝑑 ∈
{𝑎 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈ Fin ∧
((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏})) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) finSupp
(0g‘𝑅)) |
53 | 41, 43, 45, 47, 51, 52 | syl32anc 1326 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) finSupp
(0g‘𝑅)) |
54 | 12, 30 | psrbagconf1o 19195 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}–1-1-onto→{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
55 | 26, 54 | sylan 487 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}–1-1-onto→{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
56 | 1, 2, 5, 9, 39, 53, 55 | gsumf1o 18140 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) = (𝑅 Σg ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))))) |
57 | 26 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝐼 ∈ V) |
58 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
59 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
60 | 12, 30 | psrbagconcl 19194 |
. . . . . . . 8
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑐) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
61 | 57, 58, 59, 60 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑐) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
62 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))) |
63 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) = (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) |
64 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → (𝐺‘𝑒) = (𝐺‘(𝑏 ∘𝑓 − 𝑐))) |
65 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → (𝑏 ∘𝑓 − 𝑒) = (𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))) |
66 | 65 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → (𝐹‘(𝑏 ∘𝑓 − 𝑒)) = (𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))) |
67 | 64, 66 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))) = ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))))) |
68 | 61, 62, 63, 67 | fmptco 6303 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))))) |
69 | 12 | psrbagf 19186 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑏:𝐼⟶ℕ0) |
70 | 26, 69 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑏:𝐼⟶ℕ0) |
71 | 70 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑏:𝐼⟶ℕ0) |
72 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐼 ∈ V) |
73 | | elrabi 3328 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
74 | 12 | psrbagf 19186 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ V ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑐:𝐼⟶ℕ0) |
75 | 72, 73, 74 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑐:𝐼⟶ℕ0) |
76 | | nn0cn 11179 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ ℕ0
→ 𝑒 ∈
ℂ) |
77 | | nn0cn 11179 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ℕ0
→ 𝑓 ∈
ℂ) |
78 | | nncan 10189 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ ℂ ∧ 𝑓 ∈ ℂ) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
79 | 76, 77, 78 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝑒 ∈ ℕ0
∧ 𝑓 ∈
ℕ0) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
80 | 79 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ Ring
∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) ∧ (𝑒 ∈ ℕ0
∧ 𝑓 ∈
ℕ0)) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
81 | 57, 71, 75, 80 | caonncan 6833 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− (𝑏
∘𝑓 − 𝑐)) = 𝑐) |
82 | 81 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))) = (𝐹‘𝑐)) |
83 | 82 | oveq2d 6565 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))) = ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘𝑐))) |
84 | | psropprmul.s |
. . . . . . . . 9
⊢ 𝑆 =
(oppr‘𝑅) |
85 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑆) = (.r‘𝑆) |
86 | 1, 35, 84, 85 | opprmul 18449 |
. . . . . . . 8
⊢ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))) = ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘𝑐)) |
87 | 83, 86 | syl6eqr 2662 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))) = ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))) |
88 | 87 | mpteq2dva 4672 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) |
89 | 68, 88 | eqtrd 2644 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) |
90 | 89 | oveq2d 6565 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)))) = (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
91 | 8 | mptex 6390 |
. . . . . . . 8
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))) ∈ V |
92 | 91 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))) ∈ V) |
93 | | id 22 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
94 | | fvex 6113 |
. . . . . . . . 9
⊢
(oppr‘𝑅) ∈ V |
95 | 84, 94 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑆 ∈ V |
96 | 95 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑆 ∈ V) |
97 | 84, 1 | opprbas 18452 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑆) |
98 | 97 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘𝑆)) |
99 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
100 | 84, 99 | oppradd 18453 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑆) |
101 | 100 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(+g‘𝑅) =
(+g‘𝑆)) |
102 | 92, 93, 96, 98, 101 | gsumpropd 17095 |
. . . . . 6
⊢ (𝑅 ∈ Ring → (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
103 | 102 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
104 | 103 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
105 | 56, 90, 104 | 3eqtrd 2648 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
106 | 105 | mpteq2dva 4672 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))))) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))))) |
107 | | psropprmul.t |
. . 3
⊢ · =
(.r‘𝑌) |
108 | 11, 13, 35, 107, 12, 14, 20 | psrmulfval 19206 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐺 · 𝐹) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))))) |
109 | | psropprmul.z |
. . 3
⊢ 𝑍 = (𝐼 mPwSer 𝑆) |
110 | | eqid 2610 |
. . 3
⊢
(Base‘𝑍) =
(Base‘𝑍) |
111 | | psropprmul.u |
. . 3
⊢ ∙ =
(.r‘𝑍) |
112 | 97 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (Base‘𝑅) = (Base‘𝑆)) |
113 | 112 | psrbaspropd 19426 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) |
114 | 11 | fveq2i 6106 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘(𝐼 mPwSer 𝑅)) |
115 | 13, 114 | eqtri 2632 |
. . . . 5
⊢ 𝐵 = (Base‘(𝐼 mPwSer 𝑅)) |
116 | 109 | fveq2i 6106 |
. . . . 5
⊢
(Base‘𝑍) =
(Base‘(𝐼 mPwSer 𝑆)) |
117 | 113, 115,
116 | 3eqtr4g 2669 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐵 = (Base‘𝑍)) |
118 | 20, 117 | eleqtrd 2690 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ (Base‘𝑍)) |
119 | 14, 117 | eleqtrd 2690 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (Base‘𝑍)) |
120 | 109, 110,
85, 111, 12, 118, 119 | psrmulfval 19206 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))))) |
121 | 106, 108,
120 | 3eqtr4rd 2655 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) |