This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psropprmul

Description: Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses psropprmul.y ⊢ 𝑌 = ( 𝐼 mPwSer 𝑅 )
psropprmul.s ⊢ 𝑆 = ( oppr ‘ 𝑅 )
psropprmul.z ⊢ 𝑍 = ( 𝐼 mPwSer 𝑆 )
psropprmul.t ⊢ · = ( .r ‘ 𝑌 )
psropprmul.u ⊢ ∙ = ( .r ‘ 𝑍 )
psropprmul.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion psropprmul ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝐺 · 𝐹 ) )

Proof

Step Hyp Ref Expression
1 psropprmul.y ⊢ 𝑌 = ( 𝐼 mPwSer 𝑅 )
2 psropprmul.s ⊢ 𝑆 = ( oppr ‘ 𝑅 )
3 psropprmul.z ⊢ 𝑍 = ( 𝐼 mPwSer 𝑆 )
4 psropprmul.t ⊢ · = ( .r ‘ 𝑌 )
5 psropprmul.u ⊢ ∙ = ( .r ‘ 𝑍 )
6 psropprmul.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
10 9 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
11 10 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CMnd )
12 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
13 12 rabex ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∈ V
14 13 rabex ⊢ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ∈ V
15 14 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ∈ V )
16 simpll1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → 𝑅 ∈ Ring )
17 eqid ⊢ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
18 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
19 1 7 17 6 18 psrelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20 19 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝐺 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
21 elrabi ⊢ ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } → 𝑒 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
22 ffvelcdm ⊢ ( ( 𝐺 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ∧ 𝑒 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝐺 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) )
23 20 21 22 syl2an ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝐺 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) )
24 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
25 1 7 17 6 24 psrelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
26 25 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → 𝐹 : { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
27 ssrab2 ⊢ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ⊆ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin }
28 eqid ⊢ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } = { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 }
29 17 28 psrbagconcl ⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑒 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
30 29 adantll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑒 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
31 27 30 sselid ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑒 ) ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
32 26 31 ffvelcdmd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ∈ ( Base ‘ 𝑅 ) )
33 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
34 7 33 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ∈ ( Base ‘ 𝑅 ) )
35 16 23 32 34 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ∈ ( Base ‘ 𝑅 ) )
36 35 fmpttd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) : { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ⟶ ( Base ‘ 𝑅 ) )
37 mptexg ⊢ ( { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ∈ V → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ∈ V )
38 14 37 mp1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ∈ V )
39 funmpt ⊢ Fun ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) )
40 39 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → Fun ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) )
41 fvexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 0g ‘ 𝑅 ) ∈ V )
42 17 psrbaglefi ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } → { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ∈ Fin )
43 42 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ∈ Fin )
44 suppssdm ⊢ ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ dom ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) )
45 eqid ⊢ ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) = ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) )
46 45 dmmptss ⊢ dom ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 }
47 44 46 sstri ⊢ ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 }
48 47 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
49 suppssfifsupp ⊢ ( ( ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ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 ‘ 𝑅 ) )
50 38 40 41 43 48 49 syl32anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
51 17 28 psrbagconf1o ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) : { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } –1-1-onto→ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
52 51 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) : { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } –1-1-onto→ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
53 7 8 11 15 36 50 52 gsumf1o ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) ) ) )
54 17 28 psrbagconcl ⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑐 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
55 54 adantll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑐 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } )
56 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) )
57 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) = ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) )
58 fveq2 ⊢ ( 𝑒 = ( 𝑏 ∘f − 𝑐 ) → ( 𝐺 ‘ 𝑒 ) = ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) )
59 oveq2 ⊢ ( 𝑒 = ( 𝑏 ∘f − 𝑐 ) → ( 𝑏 ∘f − 𝑒 ) = ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) )
60 59 fveq2d ⊢ ( 𝑒 = ( 𝑏 ∘f − 𝑐 ) → ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) )
61 58 60 oveq12d ⊢ ( 𝑒 = ( 𝑏 ∘f − 𝑐 ) → ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) = ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) ) )
62 55 56 57 61 fmptco ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) ) ) )
63 reldmpsr ⊢ Rel dom mPwSer
64 1 6 63 strov2rcl ⊢ ( 𝐺 ∈ 𝐵 → 𝐼 ∈ V )
65 64 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐼 ∈ V )
66 65 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → 𝐼 ∈ V )
67 17 psrbagf ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } → 𝑏 : 𝐼 ⟶ ℕ0 )
68 67 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝑏 : 𝐼 ⟶ ℕ0 )
69 68 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → 𝑏 : 𝐼 ⟶ ℕ0 )
70 elrabi ⊢ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } → 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } )
71 17 psrbagf ⊢ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } → 𝑐 : 𝐼 ⟶ ℕ0 )
72 70 71 syl ⊢ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } → 𝑐 : 𝐼 ⟶ ℕ0 )
73 72 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → 𝑐 : 𝐼 ⟶ ℕ0 )
74 nn0cn ⊢ ( 𝑒 ∈ ℕ0 → 𝑒 ∈ ℂ )
75 nn0cn ⊢ ( 𝑓 ∈ ℕ0 → 𝑓 ∈ ℂ )
76 nncan ⊢ ( ( 𝑒 ∈ ℂ ∧ 𝑓 ∈ ℂ ) → ( 𝑒 − ( 𝑒 − 𝑓 ) ) = 𝑓 )
77 74 75 76 syl2an ⊢ ( ( 𝑒 ∈ ℕ0 ∧ 𝑓 ∈ ℕ0 ) → ( 𝑒 − ( 𝑒 − 𝑓 ) ) = 𝑓 )
78 77 adantl ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) ∧ ( 𝑒 ∈ ℕ0 ∧ 𝑓 ∈ ℕ0 ) ) → ( 𝑒 − ( 𝑒 − 𝑓 ) ) = 𝑓 )
79 66 69 73 78 caonncan ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) = 𝑐 )
80 79 fveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) = ( 𝐹 ‘ 𝑐 ) )
81 80 oveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑐 ) ) )
82 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
83 7 33 2 82 opprmul ⊢ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) = ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑐 ) )
84 81 83 eqtr4di ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ) → ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) ) = ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) )
85 84 mpteq2dva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − ( 𝑏 ∘f − 𝑐 ) ) ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) )
86 62 85 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) )
87 86 oveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( 𝑏 ∘f − 𝑐 ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) )
88 14 mptex ⊢ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ∈ V
89 88 a1i ⊢ ( 𝑅 ∈ Ring → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ∈ V )
90 id ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
91 2 fvexi ⊢ 𝑆 ∈ V
92 91 a1i ⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ V )
93 2 7 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 )
94 93 a1i ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
95 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
96 2 95 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 )
97 96 a1i ⊢ ( 𝑅 ∈ Ring → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 ) )
98 89 90 92 94 97 gsumpropd ⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) = ( 𝑆 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) )
99 98 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) = ( 𝑆 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) )
100 99 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) = ( 𝑆 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) )
101 53 87 100 3eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ) = ( 𝑆 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) )
102 101 mpteq2dva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) ) )
103 1 6 33 4 17 18 24 psrmulfval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 · 𝐹 ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑒 ) ) ) ) ) ) )
104 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
105 93 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
106 105 psrbaspropd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
107 1 fveq2i ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
108 6 107 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
109 3 fveq2i ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) )
110 106 108 109 3eqtr4g ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑍 ) )
111 24 110 eleqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ ( Base ‘ 𝑍 ) )
112 18 110 eleqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( Base ‘ 𝑍 ) )
113 3 104 82 5 17 111 112 psrmulfval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σg ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘f − 𝑐 ) ) ) ) ) ) )
114 102 103 113 3eqtr4rd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝐺 · 𝐹 ) )