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