Step | Hyp | Ref
| Expression |
1 | | eqid 2779 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2779 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | | ringcmn 19054 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
4 | 3 | 3ad2ant1 1113 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CMnd) |
5 | 4 | adantr 473 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑅 ∈ CMnd) |
6 | | ovex 7008 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
7 | 6 | rabex 5091 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V |
8 | 7 | rabex 5091 |
. . . . . 6
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
V |
9 | 8 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
V) |
10 | | simpll1 1192 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑅 ∈ Ring) |
11 | | psropprmul.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝐼 mPwSer 𝑅) |
12 | | eqid 2779 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
13 | | psropprmul.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑌) |
14 | | simp3 1118 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
15 | 11, 1, 12, 13, 14 | psrelbas 19873 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
16 | 15 | adantr 473 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
17 | | elrabi 3591 |
. . . . . . . 8
⊢ (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} → 𝑒 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
18 | | ffvelrn 6674 |
. . . . . . . 8
⊢ ((𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
∧ 𝑒 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐺‘𝑒) ∈ (Base‘𝑅)) |
19 | 16, 17, 18 | syl2an 586 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝐺‘𝑒) ∈ (Base‘𝑅)) |
20 | | simp2 1117 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
21 | 11, 1, 12, 13, 20 | psrelbas 19873 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
22 | 21 | ad2antrr 713 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
23 | | ssrab2 3947 |
. . . . . . . . 9
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ⊆ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
24 | | reldmpsr 19855 |
. . . . . . . . . . . . 13
⊢ Rel dom
mPwSer |
25 | 11, 13, 24 | strov2rcl 16402 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ 𝐵 → 𝐼 ∈ V) |
26 | 25 | 3ad2ant3 1115 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐼 ∈ V) |
27 | 26 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝐼 ∈ V) |
28 | | simplr 756 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
29 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
30 | | eqid 2779 |
. . . . . . . . . . 11
⊢ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} = {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} |
31 | 12, 30 | psrbagconcl 19867 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑒) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
32 | 27, 28, 29, 31 | syl3anc 1351 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑒) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
33 | 23, 32 | sseldi 3857 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑒) ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
34 | 22, 33 | ffvelrnd 6677 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝐹‘(𝑏 ∘𝑓 − 𝑒)) ∈ (Base‘𝑅)) |
35 | | eqid 2779 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
36 | 1, 35 | ringcl 19034 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘𝑒) ∈ (Base‘𝑅) ∧ (𝐹‘(𝑏 ∘𝑓 − 𝑒)) ∈ (Base‘𝑅)) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))) ∈ (Base‘𝑅)) |
37 | 10, 19, 34, 36 | syl3anc 1351 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))) ∈ (Base‘𝑅)) |
38 | 37 | fmpttd 6702 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}⟶(Base‘𝑅)) |
39 | | mptexg 6810 |
. . . . . . 7
⊢ ({𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈ V →
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∈ V) |
40 | 8, 39 | mp1i 13 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∈ V) |
41 | | funmpt 6226 |
. . . . . . 7
⊢ Fun
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) |
42 | 41 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → Fun
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) |
43 | | fvexd 6514 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(0g‘𝑅)
∈ V) |
44 | 12 | psrbaglefi 19866 |
. . . . . . 7
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
Fin) |
45 | 26, 44 | sylan 572 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ∈
Fin) |
46 | | suppssdm 7646 |
. . . . . . . 8
⊢ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ dom (𝑒 ∈
{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) |
47 | | eqid 2779 |
. . . . . . . . 9
⊢ (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) = (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) |
48 | 47 | dmmptss 5934 |
. . . . . . . 8
⊢ dom
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} |
49 | 46, 48 | sstri 3868 |
. . . . . . 7
⊢ ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} |
50 | 49 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) supp
(0g‘𝑅))
⊆ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
51 | | suppssfifsupp 8643 |
. . . . . 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‘𝑅)) |
52 | 40, 42, 43, 45, 50, 51 | syl32anc 1358 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) finSupp
(0g‘𝑅)) |
53 | 12, 30 | psrbagconf1o 19868 |
. . . . . 6
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}–1-1-onto→{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
54 | 26, 53 | sylan 572 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)):{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}–1-1-onto→{𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
55 | 1, 2, 5, 9, 38, 52, 54 | gsumf1o 18790 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) = (𝑅 Σg ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))))) |
56 | 26 | ad2antrr 713 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝐼 ∈ V) |
57 | | simplr 756 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
58 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
59 | 12, 30 | psrbagconcl 19867 |
. . . . . . . 8
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑐) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
60 | 56, 57, 58, 59 | syl3anc 1351 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− 𝑐) ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) |
61 | | eqidd 2780 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))) |
62 | | eqidd 2780 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) = (𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) |
63 | | fveq2 6499 |
. . . . . . . 8
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → (𝐺‘𝑒) = (𝐺‘(𝑏 ∘𝑓 − 𝑐))) |
64 | | oveq2 6984 |
. . . . . . . . 9
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → (𝑏 ∘𝑓 − 𝑒) = (𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))) |
65 | 64 | fveq2d 6503 |
. . . . . . . 8
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → (𝐹‘(𝑏 ∘𝑓 − 𝑒)) = (𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))) |
66 | 63, 65 | oveq12d 6994 |
. . . . . . 7
⊢ (𝑒 = (𝑏 ∘𝑓 − 𝑐) → ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))) = ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))))) |
67 | 60, 61, 62, 66 | fmptco 6714 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))))) |
68 | 12 | psrbagf 19859 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑏:𝐼⟶ℕ0) |
69 | 26, 68 | sylan 572 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑏:𝐼⟶ℕ0) |
70 | 69 | adantr 473 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑏:𝐼⟶ℕ0) |
71 | 26 | adantr 473 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐼 ∈ V) |
72 | | elrabi 3591 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
73 | 12 | psrbagf 19859 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ V ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑐:𝐼⟶ℕ0) |
74 | 71, 72, 73 | syl2an 586 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → 𝑐:𝐼⟶ℕ0) |
75 | | nn0cn 11718 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ ℕ0
→ 𝑒 ∈
ℂ) |
76 | | nn0cn 11718 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ℕ0
→ 𝑓 ∈
ℂ) |
77 | | nncan 10716 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ ℂ ∧ 𝑓 ∈ ℂ) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
78 | 75, 76, 77 | syl2an 586 |
. . . . . . . . . . . 12
⊢ ((𝑒 ∈ ℕ0
∧ 𝑓 ∈
ℕ0) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
79 | 78 | adantl 474 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ Ring
∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) ∧ (𝑒 ∈ ℕ0
∧ 𝑓 ∈
ℕ0)) → (𝑒 − (𝑒 − 𝑓)) = 𝑓) |
80 | 56, 70, 74, 79 | caonncan 7265 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝑏 ∘𝑓
− (𝑏
∘𝑓 − 𝑐)) = 𝑐) |
81 | 80 | fveq2d 6503 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → (𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))) = (𝐹‘𝑐)) |
82 | 81 | oveq2d 6992 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))) = ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘𝑐))) |
83 | | psropprmul.s |
. . . . . . . . 9
⊢ 𝑆 =
(oppr‘𝑅) |
84 | | eqid 2779 |
. . . . . . . . 9
⊢
(.r‘𝑆) = (.r‘𝑆) |
85 | 1, 35, 83, 84 | opprmul 19099 |
. . . . . . . 8
⊢ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))) = ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘𝑐)) |
86 | 82, 85 | syl6eqr 2833 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ 𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏}) → ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐)))) = ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))) |
87 | 86 | mpteq2dva 5022 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘(𝑏 ∘𝑓 − 𝑐))(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − (𝑏 ∘𝑓
− 𝑐))))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) |
88 | 67, 87 | eqtrd 2815 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐))) = (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) |
89 | 88 | oveq2d 6992 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
((𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))) ∘ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ (𝑏 ∘𝑓
− 𝑐)))) = (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
90 | 8 | mptex 6812 |
. . . . . . . 8
⊢ (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))) ∈ V |
91 | 90 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))) ∈ V) |
92 | | id 22 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
93 | 83 | fvexi 6513 |
. . . . . . . 8
⊢ 𝑆 ∈ V |
94 | 93 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑆 ∈ V) |
95 | 83, 1 | opprbas 19102 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑆) |
96 | 95 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘𝑆)) |
97 | | eqid 2779 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
98 | 83, 97 | oppradd 19103 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑆) |
99 | 98 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(+g‘𝑅) =
(+g‘𝑆)) |
100 | 91, 92, 94, 96, 99 | gsumpropd 17740 |
. . . . . 6
⊢ (𝑅 ∈ Ring → (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
101 | 100 | 3ad2ant1 1113 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
102 | 101 | adantr 473 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
103 | 55, 89, 102 | 3eqtrd 2819 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))) = (𝑆 Σg (𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐)))))) |
104 | 103 | mpteq2dva 5022 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒)))))) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))))) |
105 | | psropprmul.t |
. . 3
⊢ · =
(.r‘𝑌) |
106 | 11, 13, 35, 105, 12, 14, 20 | psrmulfval 19879 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐺 · 𝐹) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑅 Σg
(𝑒 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐺‘𝑒)(.r‘𝑅)(𝐹‘(𝑏 ∘𝑓 − 𝑒))))))) |
107 | | psropprmul.z |
. . 3
⊢ 𝑍 = (𝐼 mPwSer 𝑆) |
108 | | eqid 2779 |
. . 3
⊢
(Base‘𝑍) =
(Base‘𝑍) |
109 | | psropprmul.u |
. . 3
⊢ ∙ =
(.r‘𝑍) |
110 | 95 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (Base‘𝑅) = (Base‘𝑆)) |
111 | 110 | psrbaspropd 20106 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑆))) |
112 | 11 | fveq2i 6502 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘(𝐼 mPwSer 𝑅)) |
113 | 13, 112 | eqtri 2803 |
. . . . 5
⊢ 𝐵 = (Base‘(𝐼 mPwSer 𝑅)) |
114 | 107 | fveq2i 6502 |
. . . . 5
⊢
(Base‘𝑍) =
(Base‘(𝐼 mPwSer 𝑆)) |
115 | 111, 113,
114 | 3eqtr4g 2840 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐵 = (Base‘𝑍)) |
116 | 20, 115 | eleqtrd 2869 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ (Base‘𝑍)) |
117 | 14, 115 | eleqtrd 2869 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (Base‘𝑍)) |
118 | 107, 108,
84, 109, 12, 116, 117 | psrmulfval 19879 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝑆 Σg
(𝑐 ∈ {𝑑 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∣ 𝑑 ∘𝑟
≤ 𝑏} ↦ ((𝐹‘𝑐)(.r‘𝑆)(𝐺‘(𝑏 ∘𝑓 − 𝑐))))))) |
119 | 104, 106,
118 | 3eqtr4rd 2826 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝐺 · 𝐹)) |