Theorem psrmonprod 34117

Description: Finite product of bags of variables in a power series. Here the function 𝐺 maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026.)

Hypotheses

Ref	Expression
psrmonprod.s	⊢ 𝑆 = (𝐼 mPwSer 𝑅)
psrmonprod.b	⊢ 𝐵 = (Base‘𝑆)
psrmonprod.r	⊢ (𝜑 → 𝑅 ∈ CRing)
psrmonprod.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
psrmonprod.d	⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
psrmonprod.a	⊢ (𝜑 → 𝐴 ∈ Fin)
psrmonprod.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐷)
psrmonprod.1	⊢ 1 = (1r‘𝑅)
psrmonprod.0	⊢ 0 = (0g‘𝑅)
psrmonprod.m	⊢ 𝑀 = (mulGrp‘𝑆)
psrmonprod.g	⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))

Assertion

Ref	Expression
psrmonprod	⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))

Distinct variable groups:   0 ,ℎ,𝑦,𝑧   𝑦, 1 ,𝑧   𝐴,𝑖,𝑥,𝑦,𝑧   𝑦,𝐵,𝑧   𝐷,𝑖,𝑦,𝑧   ℎ,𝐹,𝑖,𝑥,𝑦,𝑧   𝑦,𝐺,𝑧   ℎ,𝐼,𝑦,𝑧,𝑖,𝑥   𝑅,ℎ,𝑦,𝑧   𝑦,𝑆,𝑧   𝑦,𝑉,𝑧   𝜑,𝑖,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(ℎ)   𝐴(ℎ)   𝐵(𝑥, ℎ, 𝑖)   𝐷(𝑥, ℎ)   𝑅(𝑥, 𝑖)   𝑆(𝑥, ℎ, 𝑖)   1 (𝑥, ℎ, 𝑖)   𝐺(𝑥, ℎ, 𝑖)   𝑀(𝑥, 𝑦, 𝑧, ℎ, 𝑖)   𝑉(𝑥, ℎ, 𝑖)   0 (𝑥, 𝑖)

Proof of Theorem psrmonprod

Dummy variables 𝑎 𝑏 𝑓 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psrmonprod.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶𝐷)
2	1	ffvelcdmda 7072	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐷)
3	1	feqmptd 6941	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
4		fvexd 6888	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (Base‘𝑅) ∈ V)
5		psrmonprod.d	. . . . . . . . . 10 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
6		ovex 7441	. . . . . . . . . 10 ⊢ (ℕ0 ↑m 𝐼) ∈ V
7	5, 6	rabex2 5301	. . . . . . . . 9 ⊢ 𝐷 ∈ V
8	7	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐷 ∈ V)
9		eqid 2760	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
10		psrmonprod.1	. . . . . . . . . . . 12 ⊢ 1 = (1r‘𝑅)
11		psrmonprod.r	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ CRing)
12	11	crngringd 20434	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ Ring)
13	9, 10, 12	ringidcld 20456	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (Base‘𝑅))
14	13	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → 1 ∈ (Base‘𝑅))
15		psrmonprod.0	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑅)
16	11	crnggrpd 20435	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ Grp)
17	9, 15, 16	grpidcld 33533	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (Base‘𝑅))
18	17	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → 0 ∈ (Base‘𝑅))
19	14, 18	ifcld 4528	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ 𝐷) → if(𝑧 = 𝑦, 1 , 0 ) ∈ (Base‘𝑅))
20	19	fmpttd 7103	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )):𝐷⟶(Base‘𝑅))
21	4, 8, 20	elmapdd 8839	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )) ∈ ((Base‘𝑅) ↑m 𝐷))
22		psrmonprod.s	. . . . . . . . 9 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
23	5	psrbasfsupp 34076	. . . . . . . . 9 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
24		psrmonprod.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑆)
25		psrmonprod.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
26	22, 9, 23, 24, 25	psrbas 22203	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = ((Base‘𝑅) ↑m 𝐷))
27	26	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐵 = ((Base‘𝑅) ↑m 𝐷))
28	21, 27	eleqtrrd 2863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )) ∈ 𝐵)
29		psrmonprod.g	. . . . . 6 ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))
30	28, 29	fmptd 7102	. . . . 5 ⊢ (𝜑 → 𝐺:𝐷⟶𝐵)
31	30	feqmptd 6941	. . . 4 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝐺‘𝑦)))
32		fveq2 6873	. . . 4 ⊢ (𝑦 = (𝐹‘𝑘) → (𝐺‘𝑦) = (𝐺‘(𝐹‘𝑘)))
33	2, 3, 31, 32	fmptco 7118	. . 3 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑘))))
34	33	oveq2d 7424	. 2 ⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑘)))))
35		mpteq1 5193	. . . . 5 ⊢ (𝑎 = ∅ → (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘))) = (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘))))
36	35	oveq2d 7424	. . . 4 ⊢ (𝑎 = ∅ → (𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘)))))
37		mpteq1 5193	. . . . . . 7 ⊢ (𝑎 = ∅ → (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)) = (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))
38	37	oveq2d 7424	. . . . . 6 ⊢ (𝑎 = ∅ → (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))
39	38	mpteq2dv 5198	. . . . 5 ⊢ (𝑎 = ∅ → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))))
40	39	fveq2d 6877	. . . 4 ⊢ (𝑎 = ∅ → (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))))
41	36, 40	eqeq12d 2776	. . 3 ⊢ (𝑎 = ∅ → ((𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) ↔ (𝑀 Σg (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))))))
42		mpteq1 5193	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘))) = (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘))))
43	42	oveq2d 7424	. . . 4 ⊢ (𝑎 = 𝑏 → (𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))))
44		mpteq1 5193	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)) = (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))
45	44	oveq2d 7424	. . . . . 6 ⊢ (𝑎 = 𝑏 → (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))
46	45	mpteq2dv 5198	. . . . 5 ⊢ (𝑎 = 𝑏 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))
47	46	fveq2d 6877	. . . 4 ⊢ (𝑎 = 𝑏 → (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))))
48	43, 47	eqeq12d 2776	. . 3 ⊢ (𝑎 = 𝑏 → ((𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) ↔ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))))
49		mpteq1 5193	. . . . 5 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘))) = (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘))))
50	49	oveq2d 7424	. . . 4 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → (𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘)))))
51		mpteq1 5193	. . . . . . 7 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)) = (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))
52	51	oveq2d 7424	. . . . . 6 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))
53	52	mpteq2dv 5198	. . . . 5 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))))
54	53	fveq2d 6877	. . . 4 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))))
55	50, 54	eqeq12d 2776	. . 3 ⊢ (𝑎 = (𝑏 ∪ {𝑓}) → ((𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) ↔ (𝑀 Σg (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))))))
56		mpteq1 5193	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑘))))
57	56	oveq2d 7424	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑘)))))
58		mpteq1 5193	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖)))
59	58	oveq2d 7424	. . . . . 6 ⊢ (𝑎 = 𝐴 → (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))
60	59	mpteq2dv 5198	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖)))))
61	60	fveq2d 6877	. . . 4 ⊢ (𝑎 = 𝐴 → (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))
62	57, 61	eqeq12d 2776	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑀 Σg (𝑘 ∈ 𝑎 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑎 ↦ ((𝐹‘𝑥)‘𝑖))))) ↔ (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖)))))))
63		psrmonprod.m	. . . . . 6 ⊢ 𝑀 = (mulGrp‘𝑆)
64		eqid 2760	. . . . . 6 ⊢ (1r‘𝑆) = (1r‘𝑆)
65	63, 64	ringidval 20370	. . . . 5 ⊢ (1r‘𝑆) = (0g‘𝑀)
66	65	gsum0 18834	. . . 4 ⊢ (𝑀 Σg ∅) = (1r‘𝑆)
67		mpt0 6669	. . . . . 6 ⊢ (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘))) = ∅
68	67	oveq2i 7419	. . . . 5 ⊢ (𝑀 Σg (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg ∅)
69	68	a1i 11	. . . 4 ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg ∅))
70		mpt0 6669	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)) = ∅
71	70	oveq2i 7419	. . . . . . . . . . . . . . 15 ⊢ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg ∅)
72		cnfld0 21663	. . . . . . . . . . . . . . . 16 ⊢ 0 = (0g‘ℂfld)
73	72	gsum0 18834	. . . . . . . . . . . . . . 15 ⊢ (ℂfld Σg ∅) = 0
74	71, 73	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))) = 0
75	74	mpteq2i 5200	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ 0)
76		fconstmpt 5709	. . . . . . . . . . . . 13 ⊢ (𝐼 × {0}) = (𝑖 ∈ 𝐼 ↦ 0)
77	75, 76	eqtr4i 2786	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝐼 × {0})
78	77	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝐼 × {0}))
79	78	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) ↔ 𝑦 = (𝐼 × {0})))
80	79	biimpa 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) → 𝑦 = (𝐼 × {0}))
81	80	eqeq2d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑧 = 𝑦 ↔ 𝑧 = (𝐼 × {0})))
82	81	ifbid 4505	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) → if(𝑧 = 𝑦, 1 , 0 ) = if(𝑧 = (𝐼 × {0}), 1 , 0 ))
83	82	mpteq2dv 5198	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )) = (𝑧 ∈ 𝐷 ↦ if(𝑧 = (𝐼 × {0}), 1 , 0 )))
84	22, 25, 12, 23, 15, 10, 64	psr1 22239	. . . . . . 7 ⊢ (𝜑 → (1r‘𝑆) = (𝑧 ∈ 𝐷 ↦ if(𝑧 = (𝐼 × {0}), 1 , 0 )))
85	84	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) → (1r‘𝑆) = (𝑧 ∈ 𝐷 ↦ if(𝑧 = (𝐼 × {0}), 1 , 0 )))
86	83, 85	eqtr4d 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )) = (1r‘𝑆))
87		breq1 5105	. . . . . . 7 ⊢ (ℎ = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) → (ℎ finSupp 0 ↔ (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) finSupp 0))
88		nn0ex 12581	. . . . . . . . . 10 ⊢ ℕ0 ∈ V
89	88	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℕ0 ∈ V)
90		0nn0 12590	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
91	90	fconst6 6760	. . . . . . . . . 10 ⊢ (𝐼 × {0}):𝐼⟶ℕ0
92	91	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}):𝐼⟶ℕ0)
93	89, 25, 92	elmapdd 8839	. . . . . . . 8 ⊢ (𝜑 → (𝐼 × {0}) ∈ (ℕ0 ↑m 𝐼))
94	77, 93	eqeltrid 2864	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) ∈ (ℕ0 ↑m 𝐼))
95	90	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℕ0)
96	25, 95	fczfsuppd 9356	. . . . . . . 8 ⊢ (𝜑 → (𝐼 × {0}) finSupp 0)
97	77, 96	eqbrtrid 5139	. . . . . . 7 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) finSupp 0)
98	87, 94, 97	elrabd 3646	. . . . . 6 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
99	98, 5	eleqtrrdi 2871	. . . . 5 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖)))) ∈ 𝐷)
100		fvexd 6888	. . . . 5 ⊢ (𝜑 → (1r‘𝑆) ∈ V)
101	29, 86, 99, 100	fvmptd2 6990	. . . 4 ⊢ (𝜑 → (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))) = (1r‘𝑆))
102	66, 69, 101	3eqtr4a 2821	. . 3 ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ ∅ ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ ∅ ↦ ((𝐹‘𝑥)‘𝑖))))))
103		2fveq3 6878	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → (𝐺‘(𝐹‘𝑘)) = (𝐺‘(𝐹‘𝑙)))
104	103	cbvmptv 5208	. . . . . . 7 ⊢ (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘))) = (𝑙 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑙)))
105	104	oveq2i 7419	. . . . . 6 ⊢ (𝑀 Σg (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg (𝑙 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑙))))
106	63, 24	mgpbas 20326	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑀)
107		eqid 2760	. . . . . . . . 9 ⊢ (.r‘𝑆) = (.r‘𝑆)
108	63, 107	mgpplusg 20325	. . . . . . . 8 ⊢ (.r‘𝑆) = (+g‘𝑀)
109	22, 25, 11	psrcrng 22240	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ CRing)
110	63	crngmgp 20428	. . . . . . . . . 10 ⊢ (𝑆 ∈ CRing → 𝑀 ∈ CMnd)
111	109, 110	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ CMnd)
112	111	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝑀 ∈ CMnd)
113		psrmonprod.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Fin)
114	113	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝐴 ∈ Fin)
115		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ⊆ 𝐴)
116	114, 115	ssfid 9238	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → 𝑏 ∈ Fin)
117	116	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝑏 ∈ Fin)
118	30	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) ∧ 𝑙 ∈ 𝑏) → 𝐺:𝐷⟶𝐵)
119	1	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) ∧ 𝑙 ∈ 𝑏) → 𝐹:𝐴⟶𝐷)
120		simpllr 788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝑏 ⊆ 𝐴)
121	120	sselda 3930	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) ∧ 𝑙 ∈ 𝑏) → 𝑙 ∈ 𝐴)
122	119, 121	ffvelcdmd 7073	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) ∧ 𝑙 ∈ 𝑏) → (𝐹‘𝑙) ∈ 𝐷)
123	118, 122	ffvelcdmd 7073	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) ∧ 𝑙 ∈ 𝑏) → (𝐺‘(𝐹‘𝑙)) ∈ 𝐵)
124		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝑓 ∈ (𝐴 ∖ 𝑏))
125	124	eldifbd 3911	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → ¬ 𝑓 ∈ 𝑏)
126	30	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝐺:𝐷⟶𝐵)
127	1	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝐹:𝐴⟶𝐷)
128	124	eldifad 3910	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → 𝑓 ∈ 𝐴)
129	127, 128	ffvelcdmd 7073	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → (𝐹‘𝑓) ∈ 𝐷)
130	126, 129	ffvelcdmd 7073	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → (𝐺‘(𝐹‘𝑓)) ∈ 𝐵)
131		2fveq3 6878	. . . . . . . 8 ⊢ (𝑙 = 𝑓 → (𝐺‘(𝐹‘𝑙)) = (𝐺‘(𝐹‘𝑓)))
132	106, 108, 112, 117, 123, 124, 125, 130, 131	gsumunsn 20135	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → (𝑀 Σg (𝑙 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑙)))) = ((𝑀 Σg (𝑙 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑙))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))))
133	103	cbvmptv 5208	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘))) = (𝑙 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑙)))
134	133	oveq2i 7419	. . . . . . . . . 10 ⊢ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝑀 Σg (𝑙 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑙))))
135		id 23	. . . . . . . . . 10 ⊢ ((𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))))
136	134, 135	eqtr3id 2809	. . . . . . . . 9 ⊢ ((𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑀 Σg (𝑙 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑙)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))))
137	136	oveq1d 7423	. . . . . . . 8 ⊢ ((𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))) → ((𝑀 Σg (𝑙 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑙))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))) = ((𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))))
138	137	adantl 487	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → ((𝑀 Σg (𝑙 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑙))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))) = ((𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))))
139	25	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝐼 ∈ 𝑉)
140	12	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝑅 ∈ Ring)
141		breq1 5105	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) → (ℎ finSupp 0 ↔ (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) finSupp 0))
142	88	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ℕ0 ∈ V)
143		cnfldfld 33836	. . . . . . . . . . . . . . . . 17 ⊢ ℂfld ∈ Field
144		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂfld ∈ Field → ℂfld ∈ Field)
145	144	fldcrngd 20956	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld ∈ Field → ℂfld ∈ CRing)
146		crngring 20433	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld ∈ CRing → ℂfld ∈ Ring)
147		ringcmn 20472	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
148	145, 146, 147	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (ℂfld ∈ Field → ℂfld ∈ CMnd)
149	143, 148	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ℂfld ∈ CMnd
150	149	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → ℂfld ∈ CMnd)
151	116	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → 𝑏 ∈ Fin)
152		nn0subm 21689	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ∈ (SubMnd‘ℂfld)
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → ℕ0 ∈ (SubMnd‘ℂfld))
154	5	ssrab3 4029	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐷 ⊆ (ℕ0 ↑m 𝐼)
155	1	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝐹:𝐴⟶𝐷)
156	155	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → 𝐹:𝐴⟶𝐷)
157		simpllr 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → 𝑏 ⊆ 𝐴)
158	157	sselda 3930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ 𝐴)
159	156, 158	ffvelcdmd 7073	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) ∈ 𝐷)
160	154, 159	sselid 3928	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) ∈ (ℕ0 ↑m 𝐼))
161	160	elmaprd 8848	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥):𝐼⟶ℕ0)
162		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → 𝑖 ∈ 𝐼)
163	161, 162	ffvelcdmd 7073	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → ((𝐹‘𝑥)‘𝑖) ∈ ℕ0)
164	163	fmpttd 7103	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)):𝑏⟶ℕ0)
165	90	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → 0 ∈ ℕ0)
166	164, 151, 165	fdmfifsupp 9345	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)) finSupp 0)
167	72, 150, 151, 153, 164, 166	gsumsubmcl 20094	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))) ∈ ℕ0)
168	167	fmpttd 7103	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))):𝐼⟶ℕ0)
169	142, 139, 168	elmapdd 8839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) ∈ (ℕ0 ↑m 𝐼))
170	90	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 0 ∈ ℕ0)
171	168	ffund 6702	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → Fun (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))
172	116	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝑏 ∈ Fin)
173	155	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → 𝐹:𝐴⟶𝐷)
174		simplr 781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝑏 ⊆ 𝐴)
175	174	sselda 3930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ 𝐴)
176	173, 175	ffvelcdmd 7073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) ∈ 𝐷)
177	154, 176	sselid 3928	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) ∈ (ℕ0 ↑m 𝐼))
178	177	elmaprd 8848	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥):𝐼⟶ℕ0)
179	178	feqmptd 6941	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) = (𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)))
180	179	oveq1d 7423	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → ((𝐹‘𝑥) supp 0) = ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0))
181		breq1 5105	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝐹‘𝑥) → (ℎ finSupp 0 ↔ (𝐹‘𝑥) finSupp 0))
182	176, 5	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
183	181, 182	elrabrd 3647	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥) finSupp 0)
184	183	fsuppimpd 9339	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → ((𝐹‘𝑥) supp 0) ∈ Fin)
185	180, 184	eqeltrrd 2861	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑥 ∈ 𝑏) → ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0) ∈ Fin)
186	185	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ∀𝑥 ∈ 𝑏 ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0) ∈ Fin)
187		iunfi 9310	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ Fin ∧ ∀𝑥 ∈ 𝑏 ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0) ∈ Fin) → ∪ 𝑥 ∈ 𝑏 ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0) ∈ Fin)
188	172, 186, 187	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ∪ 𝑥 ∈ 𝑏 ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0) ∈ Fin)
189		cmnmnd 19972	. . . . . . . . . . . . . . . . 17 ⊢ (ℂfld ∈ CMnd → ℂfld ∈ Mnd)
190	149, 189	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ℂfld ∈ Mnd
191	190	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ℂfld ∈ Mnd)
192	114	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝐴 ∈ Fin)
193	192, 174	ssexd 5285	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝑏 ∈ V)
194	72, 191, 193, 139, 163	suppgsumssiun 33566	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) supp 0) ⊆ ∪ 𝑥 ∈ 𝑏 ((𝑖 ∈ 𝐼 ↦ ((𝐹‘𝑥)‘𝑖)) supp 0))
195	188, 194	ssfid 9238	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) supp 0) ∈ Fin)
196	169, 170, 171, 195	isfsuppd 9336	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) finSupp 0)
197	141, 169, 196	elrabd 3646	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
198	197, 5	eleqtrrdi 2871	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) ∈ 𝐷)
199		difssd 4083	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ⊆ 𝐴) → (𝐴 ∖ 𝑏) ⊆ 𝐴)
200	199	sselda 3930	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → 𝑓 ∈ 𝐴)
201	155, 200	ffvelcdmd 7073	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝐹‘𝑓) ∈ 𝐷)
202	22, 24, 15, 10, 5, 139, 140, 198, 107, 201, 29	psrmonmul2 34116	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ((𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))) = (𝐺‘((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) ∘f + (𝐹‘𝑓))))
203	168	ffnd 6698	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) Fn 𝐼)
204	154, 201	sselid 3928	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝐹‘𝑓) ∈ (ℕ0 ↑m 𝐼))
205	204	elmaprd 8848	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝐹‘𝑓):𝐼⟶ℕ0)
206	205	ffnd 6698	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝐹‘𝑓) Fn 𝐼)
207		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏))
208		ovexd 7443	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑖 ∈ 𝐼) → (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))) ∈ V)
209		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))
210	207, 208, 209	fnmptd 6668	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))) Fn 𝐼)
211		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))
212		fveq2 6873	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((𝐹‘𝑥)‘𝑖) = ((𝐹‘𝑥)‘𝑗))
213	212	mpteq2dv 5198	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)) = (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑗)))
214	213	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑗))))
215		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
216		ovexd 7443	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑗))) ∈ V)
217	211, 214, 215, 216	fvmptd3 7005	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))‘𝑗) = (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑗))))
218		eqidd 2761	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ((𝐹‘𝑓)‘𝑗) = ((𝐹‘𝑓)‘𝑗))
219	212	mpteq2dv 5198	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)) = (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑗)))
220	219	oveq2d 7424	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))) = (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑗))))
221		ovexd 7443	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑗))) ∈ V)
222	209, 220, 215, 221	fvmptd3 7005	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))‘𝑗) = (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑗))))
223		cnfldbas 21643	. . . . . . . . . . . . 13 ⊢ ℂ = (Base‘ℂfld)
224		cnfldadd 21645	. . . . . . . . . . . . 13 ⊢ + = (+g‘ℂfld)
225	149	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ℂfld ∈ CMnd)
226	172	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → 𝑏 ∈ Fin)
227	178	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥):𝐼⟶ℕ0)
228		nn0sscn 12580	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 ⊆ ℂ
229	228	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → ℕ0 ⊆ ℂ)
230	227, 229	fssd 6715	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → (𝐹‘𝑥):𝐼⟶ℂ)
231		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → 𝑗 ∈ 𝐼)
232	230, 231	ffvelcdmd 7073	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝑏) → ((𝐹‘𝑥)‘𝑗) ∈ ℂ)
233		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → 𝑓 ∈ (𝐴 ∖ 𝑏))
234	233	eldifbd 3911	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ¬ 𝑓 ∈ 𝑏)
235	205	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑓):𝐼⟶ℕ0)
236	228	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ℕ0 ⊆ ℂ)
237	235, 236	fssd 6715	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑓):𝐼⟶ℂ)
238	237, 215	ffvelcdmd 7073	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ((𝐹‘𝑓)‘𝑗) ∈ ℂ)
239		fveq2 6873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑓 → (𝐹‘𝑥) = (𝐹‘𝑓))
240	239	fveq1d 6875	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑓 → ((𝐹‘𝑥)‘𝑗) = ((𝐹‘𝑓)‘𝑗))
241	223, 224, 225, 226, 232, 233, 234, 238, 240	gsumunsn 20135	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑗))) = ((ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑗))) + ((𝐹‘𝑓)‘𝑗)))
242	222, 241	eqtr2d 2796	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ 𝑗 ∈ 𝐼) → ((ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑗))) + ((𝐹‘𝑓)‘𝑗)) = ((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))‘𝑗))
243	139, 203, 206, 210, 217, 218, 242	offveq 7702	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) ∘f + (𝐹‘𝑓)) = (𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))))
244	243	fveq2d 6877	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → (𝐺‘((𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))) ∘f + (𝐹‘𝑓))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))))
245	202, 244	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ((𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))))
246	245	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → ((𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))(.r‘𝑆)(𝐺‘(𝐹‘𝑓))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))))
247	132, 138, 246	3eqtrd 2799	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → (𝑀 Σg (𝑙 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑙)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))))
248	105, 247	eqtrid 2807	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) ∧ (𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖)))))) → (𝑀 Σg (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖))))))
249	248	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ⊆ 𝐴) ∧ 𝑓 ∈ (𝐴 ∖ 𝑏)) → ((𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑀 Σg (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))))))
250	249	anasss 472	. . 3 ⊢ ((𝜑 ∧ (𝑏 ⊆ 𝐴 ∧ 𝑓 ∈ (𝐴 ∖ 𝑏))) → ((𝑀 Σg (𝑘 ∈ 𝑏 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝑏 ↦ ((𝐹‘𝑥)‘𝑖))))) → (𝑀 Σg (𝑘 ∈ (𝑏 ∪ {𝑓}) ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ (𝑏 ∪ {𝑓}) ↦ ((𝐹‘𝑥)‘𝑖)))))))
251	41, 48, 55, 62, 102, 250, 113	findcard2d 9160	. 2 ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑘)))) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))
252	34, 251	eqtrd 2795	1 ⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412  Vcvv 3450   ∖ cdif 3895   ∪ cun 3896   ⊆ wss 3898  ∅c0 4278  ifcif 4481  {csn 4583  ∪ ciun 4950   class class class wbr 5102   ↦ cmpt 5185   × cxp 5645   ∘ ccom 5651  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408   ∘_f cof 7674   supp csupp 8155   ↑_m cmap 8825  Fincfn 8951   finSupp cfsupp 9331  ℂcc 11169  0cc0 11171   + caddc 11174  ℕ₀cn0 12575  Basecbs 17348  ._rcmulr 17390  0_gc0g 17571   Σ_g cgsu 17572  Mndcmnd 18884  SubMndcsubmnd 18938  CMndccmn 19955  mulGrpcmgp 20321  1_rcur 20368  Ringcrg 20420  CRingccrg 20421  Fieldcfield 20942  ℂ_fldccnfld 21639   mPwSer cmps 22173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247  ax-pre-mulgt0 11248  ax-addf 11250

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7676  df-ofr 7677  df-om 7861  df-1st 7984  df-2nd 7985  df-supp 8156  df-tpos 8221  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-2o 8455  df-er 8695  df-map 8827  df-pm 8828  df-ixp 8904  df-en 8952  df-dom 8953  df-sdom 8954  df-fin 8955  df-fsupp 9332  df-sup 9412  df-oi 9482  df-card 9991  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-sub 11514  df-neg 11515  df-div 11943  df-nn 12305  df-2 12374  df-3 12375  df-4 12376  df-5 12377  df-6 12378  df-7 12379  df-8 12380  df-9 12381  df-n0 12576  df-z 12663  df-dec 12784  df-uz 12935  df-fz 13609  df-fzo 13757  df-seq 14113  df-hash 14442  df-struct 17286  df-sets 17303  df-slot 17321  df-ndx 17333  df-base 17349  df-ress 17370  df-plusg 17402  df-mulr 17403  df-starv 17404  df-sca 17405  df-vsca 17406  df-ip 17407  df-tset 17408  df-ple 17409  df-ds 17411  df-unif 17412  df-hom 17413  df-cco 17414  df-0g 17573  df-gsum 17574  df-prds 17579  df-pws 17581  df-mre 17717  df-mrc 17718  df-acs 17720  df-mgm 18777  df-sgrp 18869  df-mnd 18885  df-mhm 18939  df-submnd 18940  df-grp 19108  df-minusg 19109  df-mulg 19239  df-ghm 19389  df-cntz 19492  df-cmn 19957  df-abl 19958  df-mgp 20322  df-rng 20336  df-ur 20369  df-ring 20422  df-cring 20423  df-oppr 20528  df-dvdsr 20548  df-unit 20549  df-invr 20579  df-dvr 20592  df-drng 20943  df-field 20944  df-cnfld 21640  df-psr 22178

This theorem is used by:  mplmonprod  34119