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	⊢ 𝑆 = ( opp_r ‘ 𝑅 )
	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	⊢ 𝑆 = ( opp_r ‘ 𝑅 )
3		psropprmul.z	⊢ 𝑍 = ( 𝐼 mPwSer 𝑆 )
4		psropprmul.t	⊢ · = ( ._r ‘ 𝑌 )
5		psropprmul.u	⊢ ∙ = ( ._r ‘ 𝑍 )
6		psropprmul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
9		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
10	9	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
11	10	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CMnd )
12		ovex	⊢ ( ℕ₀ ↑_m 𝐼 ) ∈ V
13	12	rabex	⊢ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∈ V
14	13	rabex	⊢ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ∈ V
15	14	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ∈ V )
16		simpll1	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → 𝑅 ∈ Ring )
17		eqid	⊢ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } = { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin }
18		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
19	1 7 17 6 18	psrelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 : { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
20	19	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝐺 : { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
21		elrabi	⊢ ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } → 𝑒 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } )
22		ffvelcdm	⊢ ( ( 𝐺 : { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) ∧ 𝑒 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝐺 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) )
23	20 21 22	syl2an	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝐺 ‘ 𝑒 ) ∈ ( Base ‘ 𝑅 ) )
24		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
25	1 7 17 6 24	psrelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 : { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
26	25	ad2antrr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → 𝐹 : { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
27		ssrab2	⊢ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ⊆ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin }
28		eqid	⊢ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } = { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 }
29	17 28	psrbagconcl	⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝑏 ∘_f − 𝑒 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
30	29	adantll	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝑏 ∘_f − 𝑒 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
31	27 30	sselid	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝑏 ∘_f − 𝑒 ) ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } )
32	26 31	ffvelcdmd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ∈ ( Base ‘ 𝑅 ) )
36	35	fmpttd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) : { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ⟶ ( Base ‘ 𝑅 ) )
37		mptexg	⊢ ( { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ∈ V → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∈ V )
38	14 37	mp1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∈ V )
39		funmpt	⊢ Fun ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) )
40	39	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → Fun ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) )
41		fvexd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 0_g ‘ 𝑅 ) ∈ V )
42	17	psrbaglefi	⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } → { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ∈ Fin )
43	42	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ∈ Fin )
44		suppssdm	⊢ ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ dom ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) )
45		eqid	⊢ ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) = ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) )
46	45	dmmptss	⊢ dom ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 }
47	44 46	sstri	⊢ ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 }
48	47	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
49		suppssfifsupp	⊢ ( ( ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∈ V ∧ Fun ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∧ ( 0_g ‘ 𝑅 ) ∈ V ) ∧ ( { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ∈ Fin ∧ ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
50	38 40 41 43 48 49	syl32anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
51	17 28	psrbagconf1o	⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) : { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } –1-1-onto→ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
52	51	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) : { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } –1-1-onto→ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
53	7 8 11 15 36 50 52	gsumf1o	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σ_g ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ) = ( 𝑅 Σ_g ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) ) ) )
54	17 28	psrbagconcl	⊢ ( ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝑏 ∘_f − 𝑐 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
55	54	adantll	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝑏 ∘_f − 𝑐 ) ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } )
56		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) )
57		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) = ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → 𝐼 ∈ V )
67	17	psrbagf	⊢ ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } → 𝑏 : 𝐼 ⟶ ℕ₀ )
68	67	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → 𝑏 : 𝐼 ⟶ ℕ₀ )
69	68	adantr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → 𝑏 : 𝐼 ⟶ ℕ₀ )
70		elrabi	⊢ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } → 𝑐 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } )
71	17	psrbagf	⊢ ( 𝑐 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } → 𝑐 : 𝐼 ⟶ ℕ₀ )
72	70 71	syl	⊢ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } → 𝑐 : 𝐼 ⟶ ℕ₀ )
73	72	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → 𝑐 : 𝐼 ⟶ ℕ₀ )
74		nn0cn	⊢ ( 𝑒 ∈ ℕ₀ → 𝑒 ∈ ℂ )
75		nn0cn	⊢ ( 𝑓 ∈ ℕ₀ → 𝑓 ∈ ℂ )
76		nncan	⊢ ( ( 𝑒 ∈ ℂ ∧ 𝑓 ∈ ℂ ) → ( 𝑒 − ( 𝑒 − 𝑓 ) ) = 𝑓 )
77	74 75 76	syl2an	⊢ ( ( 𝑒 ∈ ℕ₀ ∧ 𝑓 ∈ ℕ₀ ) → ( 𝑒 − ( 𝑒 − 𝑓 ) ) = 𝑓 )
78	77	adantl	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) ∧ ( 𝑒 ∈ ℕ₀ ∧ 𝑓 ∈ ℕ₀ ) ) → ( 𝑒 − ( 𝑒 − 𝑓 ) ) = 𝑓 )
79	66 69 73 78	caonncan	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝑏 ∘_f − ( 𝑏 ∘_f − 𝑐 ) ) = 𝑐 )
80	79	fveq2d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( 𝐹 ‘ ( 𝑏 ∘_f − ( 𝑏 ∘_f − 𝑐 ) ) ) = ( 𝐹 ‘ 𝑐 ) )
81	80	oveq2d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) ∧ 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ) → ( ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − ( 𝑏 ∘_f − 𝑐 ) ) ) ) = ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) )
85	84	mpteq2dva	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) )
86	62 85	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) )
87	86	oveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σ_g ( ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( 𝑏 ∘_f − 𝑐 ) ) ) ) = ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) )
88	14	mptex	⊢ ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ∈ V
89	88	a1i	⊢ ( 𝑅 ∈ Ring → ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_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 ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) = ( 𝑆 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) )
99	98	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) = ( 𝑆 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) )
100	99	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) = ( 𝑆 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) )
101	53 87 100	3eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σ_g ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ) = ( 𝑆 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) )
102	101	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σ_g ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐺 ‘ 𝑒 ) ( ._r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘_f − 𝑒 ) ) ) ) ) ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) ) )
103	1 6 33 4 17 18 24	psrmulfval	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 · 𝐹 ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σ_g ( 𝑒 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝑏 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ↦ ( 𝑆 Σ_g ( 𝑐 ∈ { 𝑑 ∈ { 𝑎 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin } ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) ( ._r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) ) )
114	102 103 113	3eqtr4rd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝐺 · 𝐹 ) )

Metamath Proof Explorer

Theorem psropprmul

Proof