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

Metamath Proof Explorer

Theorem psrmonprod

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

Ref Expression
Hypotheses 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 psrmonprod ( 𝜑 → ( 𝑀 Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrmonprod.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmonprod.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrmonprod.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 psrmonprod.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 psrmonprod.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6 psrmonprod.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
7 psrmonprod.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐷 )
8 psrmonprod.1 ⊢ 1 = ( 1r ‘ 𝑅 )
9 psrmonprod.0 ⊢ 0 = ( 0g ‘ 𝑅 )
10 psrmonprod.m ⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
11 psrmonprod.g ⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
12 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐷 )
13 7 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
14 fvexd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( Base ‘ 𝑅 ) ∈ V )
15 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
16 5 15 rabex2 ⊢ 𝐷 ∈ V
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐷 ∈ V )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 3 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
20 18 8 19 ringidcld ⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → 1 ∈ ( Base ‘ 𝑅 ) )
22 3 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
23 18 9 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
24 22 23 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → 0 ∈ ( Base ‘ 𝑅 ) )
26 21 25 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → if ( 𝑧 = 𝑦 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
27 26 fmpttd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
28 14 17 27 elmapdd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
29 5 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
30 1 18 29 2 4 psrbas ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
32 28 31 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ 𝐵 )
33 32 11 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ 𝐵 )
34 33 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝐺 ‘ 𝑦 ) ) )
35 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
36 12 13 34 35 fmptco ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
37 36 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
38 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
39 38 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
40 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) )
41 40 oveq2d ⊢ ( 𝑎 = ∅ → ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) )
42 41 mpteq2dv ⊢ ( 𝑎 = ∅ → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) )
43 42 fveq2d ⊢ ( 𝑎 = ∅ → ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
44 39 43 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) )
45 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
46 45 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
47 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) )
48 47 oveq2d ⊢ ( 𝑎 = 𝑏 → ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) )
49 48 mpteq2dv ⊢ ( 𝑎 = 𝑏 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) )
50 49 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
51 46 50 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) )
52 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
53 52 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
54 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) )
55 54 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) )
56 55 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) )
57 56 fveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
58 53 57 eqeq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) )
59 mpteq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
60 59 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
61 mpteq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) )
62 61 oveq2d ⊢ ( 𝑎 = 𝐴 → ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) )
63 62 mpteq2dv ⊢ ( 𝑎 = 𝐴 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) )
64 63 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
65 60 64 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) )
66 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
67 10 66 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑀 )
68 67 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑆 )
69 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ∅
70 69 oveq2i ⊢ ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ∅ )
71 70 a1i ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ∅ ) )
72 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ∅
73 72 oveq2i ⊢ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ∅ )
74 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
75 74 gsum0 ⊢ ( ℂfld Σg ∅ ) = 0
76 73 75 eqtri ⊢ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = 0
77 76 mpteq2i ⊢ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ 0 )
78 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑖 ∈ 𝐼 ↦ 0 )
79 77 78 eqtr4i ⊢ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝐼 × { 0 } )
80 79 a1i ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝐼 × { 0 } ) )
81 80 eqeq2d ⊢ ( 𝜑 → ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ↔ 𝑦 = ( 𝐼 × { 0 } ) ) )
82 81 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → 𝑦 = ( 𝐼 × { 0 } ) )
83 82 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑧 = 𝑦 ↔ 𝑧 = ( 𝐼 × { 0 } ) ) )
84 83 ifbid ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
85 84 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
86 1 4 19 29 9 8 66 psr1 ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 1r ‘ 𝑆 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
88 85 87 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 1r ‘ 𝑆 ) )
89 breq1 ⊢ ( ℎ = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) → ( ℎ finSupp 0 ↔ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) finSupp 0 ) )
90 nn0ex ⊢ ℕ0 ∈ V
91 90 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
92 0nn0 ⊢ 0 ∈ ℕ0
93 92 fconst6 ⊢ ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0
94 93 a1i ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) : 𝐼 ⟶ ℕ0 )
95 91 4 94 elmapdd ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ ( ℕ0 ↑m 𝐼 ) )
96 79 95 eqeltrid ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∈ ( ℕ0 ↑m 𝐼 ) )
97 92 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
98 4 97 fczfsuppd ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) finSupp 0 )
99 79 98 eqbrtrid ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) finSupp 0 )
100 89 96 99 elrabd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
101 100 5 eleqtrrdi ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∈ 𝐷 )
102 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ V )
103 11 88 101 102 fvmptd2 ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) = ( 1r ‘ 𝑆 ) )
104 68 71 103 3eqtr4a ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
105 2fveq3 ⊢ ( 𝑘 = 𝑙 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) )
106 105 cbvmptv ⊢ ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) )
107 106 oveq2i ⊢ ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) )
108 10 2 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
109 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
110 10 109 mgpplusg ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ 𝑀 )
111 1 4 3 psrcrng ⊢ ( 𝜑 → 𝑆 ∈ CRing )
112 10 crngmgp ⊢ ( 𝑆 ∈ CRing → 𝑀 ∈ CMnd )
113 111 112 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
114 113 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝑀 ∈ CMnd )
115 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝐴 ∈ Fin )
116 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ⊆ 𝐴 )
117 115 116 ssfid ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ∈ Fin )
118 117 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝑏 ∈ Fin )
119 33 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → 𝐺 : 𝐷 ⟶ 𝐵 )
120 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → 𝐹 : 𝐴 ⟶ 𝐷 )
121 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝑏 ⊆ 𝐴 )
122 121 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → 𝑙 ∈ 𝐴 )
123 120 122 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑙 ) ∈ 𝐷 )
124 119 123 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ∈ 𝐵 )
125 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
126 125 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ¬ 𝑓 ∈ 𝑏 )
127 33 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝐺 : 𝐷 ⟶ 𝐵 )
128 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝐹 : 𝐴 ⟶ 𝐷 )
129 125 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → 𝑓 ∈ 𝐴 )
130 128 129 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( 𝐹 ‘ 𝑓 ) ∈ 𝐷 )
131 127 130 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ 𝐵 )
132 2fveq3 ⊢ ( 𝑙 = 𝑓 → ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) )
133 108 110 114 118 124 125 126 131 132 gsumunsn ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( 𝑀 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) ) = ( ( 𝑀 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
134 105 cbvmptv ⊢ ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑙 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) )
135 134 oveq2i ⊢ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑀 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) )
136 id ⊢ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
137 135 136 eqtr3id ⊢ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑀 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
138 137 oveq1d ⊢ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( ( 𝑀 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) = ( ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
139 138 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( ( 𝑀 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) = ( ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
140 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝐼 ∈ 𝑉 )
141 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑅 ∈ Ring )
142 breq1 ⊢ ( ℎ = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) → ( ℎ finSupp 0 ↔ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) finSupp 0 ) )
143 90 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ℕ0 ∈ V )
144 cnfldfld ⊢ ℂfld ∈ Field
145 id ⊢ ( ℂfld ∈ Field → ℂfld ∈ Field )
146 145 fldcrngd ⊢ ( ℂfld ∈ Field → ℂfld ∈ CRing )
147 crngring ⊢ ( ℂfld ∈ CRing → ℂfld ∈ Ring )
148 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
149 146 147 148 3syl ⊢ ( ℂfld ∈ Field → ℂfld ∈ CMnd )
150 144 149 ax-mp ⊢ ℂfld ∈ CMnd
151 150 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → ℂfld ∈ CMnd )
152 117 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝑏 ∈ Fin )
153 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
154 153 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
155 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → 𝐼 ∈ 𝑉 )
156 90 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ℕ0 ∈ V )
157 5 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
158 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐷 )
159 158 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → 𝐹 : 𝐴 ⟶ 𝐷 )
160 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝑏 ⊆ 𝐴 )
161 160 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → 𝑥 ∈ 𝐴 )
162 159 161 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
163 157 162 sselid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℕ0 ↑m 𝐼 ) )
164 155 156 163 elmaprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) : 𝐼 ⟶ ℕ0 )
165 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → 𝑖 ∈ 𝐼 )
166 164 165 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ∈ ℕ0 )
167 166 fmpttd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) : 𝑏 ⟶ ℕ0 )
168 92 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → 0 ∈ ℕ0 )
169 167 152 168 fdmfifsupp ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) finSupp 0 )
170 74 151 152 154 167 169 gsumsubmcl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ∈ ℕ0 )
171 170 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) : 𝐼 ⟶ ℕ0 )
172 143 140 171 elmapdd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∈ ( ℕ0 ↑m 𝐼 ) )
173 92 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 0 ∈ ℕ0 )
174 171 ffund ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → Fun ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) )
175 117 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑏 ∈ Fin )
176 140 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝐼 ∈ 𝑉 )
177 90 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ℕ0 ∈ V )
178 158 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝐹 : 𝐴 ⟶ 𝐷 )
179 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑏 ⊆ 𝐴 )
180 179 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝑥 ∈ 𝐴 )
181 178 180 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
182 157 181 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℕ0 ↑m 𝐼 ) )
183 176 177 182 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) : 𝐼 ⟶ ℕ0 )
184 183 feqmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) )
185 184 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) supp 0 ) = ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) )
186 breq1 ⊢ ( ℎ = ( 𝐹 ‘ 𝑥 ) → ( ℎ finSupp 0 ↔ ( 𝐹 ‘ 𝑥 ) finSupp 0 ) )
187 181 5 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
188 186 187 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) finSupp 0 )
189 188 fsuppimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) supp 0 ) ∈ Fin )
190 185 189 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) ∈ Fin )
191 190 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ∀ 𝑥 ∈ 𝑏 ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) ∈ Fin )
192 iunfi ⊢ ( ( 𝑏 ∈ Fin ∧ ∀ 𝑥 ∈ 𝑏 ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) ∈ Fin ) → ∪ 𝑥 ∈ 𝑏 ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) ∈ Fin )
193 175 191 192 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ∪ 𝑥 ∈ 𝑏 ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) ∈ Fin )
194 cmnmnd ⊢ ( ℂfld ∈ CMnd → ℂfld ∈ Mnd )
195 150 194 ax-mp ⊢ ℂfld ∈ Mnd
196 195 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ℂfld ∈ Mnd )
197 115 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝐴 ∈ Fin )
198 197 179 ssexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑏 ∈ V )
199 74 196 198 140 166 suppgsumssiun ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) supp 0 ) ⊆ ∪ 𝑥 ∈ 𝑏 ( ( 𝑖 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) supp 0 ) )
200 193 199 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) supp 0 ) ∈ Fin )
201 172 173 174 200 isfsuppd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) finSupp 0 )
202 142 172 201 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
203 202 5 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∈ 𝐷 )
204 difssd ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( 𝐴 ∖ 𝑏 ) ⊆ 𝐴 )
205 204 sselda ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑓 ∈ 𝐴 )
206 158 205 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑓 ) ∈ 𝐷 )
207 1 2 9 8 5 140 141 203 109 206 11 psrmonmul2 ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) = ( 𝐺 ‘ ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∘f + ( 𝐹 ‘ 𝑓 ) ) ) )
208 171 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) Fn 𝐼 )
209 157 206 sselid ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑓 ) ∈ ( ℕ0 ↑m 𝐼 ) )
210 140 143 209 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑓 ) : 𝐼 ⟶ ℕ0 )
211 210 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑓 ) Fn 𝐼 )
212 nfv ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
213 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ∈ V )
214 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) )
215 212 213 214 fnmptd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) Fn 𝐼 )
216 eqid ⊢ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) )
217 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) )
218 217 mpteq2dv ⊢ ( 𝑖 = 𝑗 → ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) )
219 218 oveq2d ⊢ ( 𝑖 = 𝑗 → ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) )
220 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ 𝐼 )
221 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) ∈ V )
222 216 219 220 221 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ‘ 𝑗 ) = ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) )
223 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑗 ) )
224 217 mpteq2dv ⊢ ( 𝑖 = 𝑗 → ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) )
225 224 oveq2d ⊢ ( 𝑖 = 𝑗 → ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) = ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) )
226 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) ∈ V )
227 214 225 220 226 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ‘ 𝑗 ) = ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) )
228 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
229 cnfldadd ⊢ + = ( +g ‘ ℂfld )
230 150 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ℂfld ∈ CMnd )
231 175 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → 𝑏 ∈ Fin )
232 183 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) : 𝐼 ⟶ ℕ0 )
233 nn0sscn ⊢ ℕ0 ⊆ ℂ
234 233 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ℕ0 ⊆ ℂ )
235 232 234 fssd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑥 ) : 𝐼 ⟶ ℂ )
236 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → 𝑗 ∈ 𝐼 )
237 235 236 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ∈ ℂ )
238 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
239 238 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ¬ 𝑓 ∈ 𝑏 )
240 210 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑓 ) : 𝐼 ⟶ ℕ0 )
241 233 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ℕ0 ⊆ ℂ )
242 240 241 fssd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑓 ) : 𝐼 ⟶ ℂ )
243 242 220 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑗 ) ∈ ℂ )
244 fveq2 ⊢ ( 𝑥 = 𝑓 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑓 ) )
245 244 fveq1d ⊢ ( 𝑥 = 𝑓 → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑗 ) )
246 228 229 230 231 237 238 239 243 245 gsumunsn ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) = ( ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) + ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑗 ) ) )
247 227 246 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑗 ) ) ) + ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑗 ) ) = ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ‘ 𝑗 ) )
248 140 208 211 215 222 223 247 offveq ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∘f + ( 𝐹 ‘ 𝑓 ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) )
249 248 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐺 ‘ ( ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ∘f + ( 𝐹 ‘ 𝑓 ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
250 207 249 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
251 250 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ ( 𝐹 ‘ 𝑓 ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
252 133 139 251 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( 𝑀 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑙 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
253 107 252 eqtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
254 253 ex ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) )
255 254 anasss ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) ) )
256 44 51 58 65 104 255 6 findcard2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
257 37 256 eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )