Metamath Proof Explorer

Theorem evlextv

Description: Evaluating a variable-extended polynomial is the same as evaluating the polynomial in the original set of variables (in both cases, the additionial variable is ignored). (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses evlextv.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
evlextv.o ⊢ 𝑂 = ( 𝐽 eval 𝑅 )
evlextv.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
evlextv.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
evlextv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evlextv.e ⊢ 𝐸 = ( 𝐼 extendVars 𝑅 )
evlextv.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evlextv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlextv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
evlextv.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
evlextv.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐵 )
Assertion evlextv ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ) ‘ 𝐴 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐴 ↾ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 evlextv.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2 evlextv.o ⊢ 𝑂 = ( 𝐽 eval 𝑅 )
3 evlextv.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
4 evlextv.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
5 evlextv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 evlextv.e ⊢ 𝐸 = ( 𝐼 extendVars 𝑅 )
7 evlextv.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
8 evlextv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9 evlextv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
10 evlextv.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
11 evlextv.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐵 )
12 6 fveq1i ⊢ ( 𝐸 ‘ 𝑌 ) = ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 )
13 12 fveq1i ⊢ ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) = ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 )
14 13 fveq1i ⊢ ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 )
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) )
16 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
17 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18 8 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝐼 ∈ 𝑉 )
19 7 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑅 ∈ CRing )
20 9 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑌 ∈ 𝐼 )
21 10 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝐹 ∈ 𝑀 )
22 breq1 ⊢ ( ℎ = 𝑐 → ( ℎ finSupp 0 ↔ 𝑐 finSupp 0 ) )
23 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ⊆ ( ℕ0 ↑m 𝐼 )
24 23 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ⊆ ( ℕ0 ↑m 𝐼 ) )
25 24 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) )
26 fveq1 ⊢ ( ℎ = 𝑐 → ( ℎ ‘ 𝑌 ) = ( 𝑐 ‘ 𝑌 ) )
27 26 eqeq1d ⊢ ( ℎ = 𝑐 → ( ( ℎ ‘ 𝑌 ) = 0 ↔ ( 𝑐 ‘ 𝑌 ) = 0 ) )
28 22 27 anbi12d ⊢ ( ℎ = 𝑐 → ( ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) ↔ ( 𝑐 finSupp 0 ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) ) )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } )
30 28 29 elrabrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑐 finSupp 0 ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) )
31 30 simpld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑐 finSupp 0 )
32 22 25 31 elrabd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
33 16 17 18 19 20 3 4 21 32 extvfvv ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = if ( ( 𝑐 ‘ 𝑌 ) = 0 , ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) )
34 30 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑐 ‘ 𝑌 ) = 0 )
35 34 iftrued ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → if ( ( 𝑐 ‘ 𝑌 ) = 0 , ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) )
36 15 33 35 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) )
37 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
38 37 5 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
39 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
40 37 39 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
41 37 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
42 19 41 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
43 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) )
44 3 difeq2i ⊢ ( 𝐼 ∖ 𝐽 ) = ( 𝐼 ∖ ( 𝐼 ∖ { 𝑌 } ) )
45 9 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝐼 )
46 dfss4 ⊢ ( { 𝑌 } ⊆ 𝐼 ↔ ( 𝐼 ∖ ( 𝐼 ∖ { 𝑌 } ) ) = { 𝑌 } )
47 45 46 sylib ⊢ ( 𝜑 → ( 𝐼 ∖ ( 𝐼 ∖ { 𝑌 } ) ) = { 𝑌 } )
48 44 47 eqtrid ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) = { 𝑌 } )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝐼 ∖ 𝐽 ) = { 𝑌 } )
50 43 49 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑖 ∈ { 𝑌 } )
51 50 elsnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑖 = 𝑌 )
52 51 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑌 ) )
53 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝑐 ‘ 𝑌 ) = 0 )
54 52 53 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝑐 ‘ 𝑖 ) = 0 )
55 54 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) )
56 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐴 : 𝐼 ⟶ 𝐵 )
57 difssd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝐼 ∖ 𝐽 ) ⊆ 𝐼 )
58 57 sselda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑖 ∈ 𝐼 )
59 56 58 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 )
60 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
61 38 40 60 mulg0 ⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) = ( 1r ‘ 𝑅 ) )
62 59 61 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) = ( 1r ‘ 𝑅 ) )
63 55 62 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) = ( 1r ‘ 𝑅 ) )
64 fvexd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 1r ‘ 𝑅 ) ∈ V )
65 0nn0 ⊢ 0 ∈ ℕ0
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ0 )
67 8 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
68 ssidd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ⊆ 𝐼 )
69 11 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐴 : 𝐼 ⟶ 𝐵 )
70 69 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 )
71 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 )
72 71 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐼 ) )
73 72 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) )
74 73 elmaprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑐 : 𝐼 ⟶ ℕ0 )
75 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
76 22 75 elrabrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑐 finSupp 0 )
77 38 40 60 mulg0 ⊢ ( 𝑥 ∈ 𝐵 → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
78 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
79 64 66 67 68 70 74 76 78 fisuppov1 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) finSupp ( 1r ‘ 𝑅 ) )
80 32 79 syldan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) finSupp ( 1r ‘ 𝑅 ) )
81 7 41 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
83 82 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
84 83 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
85 74 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑐 ‘ 𝑖 ) ∈ ℕ0 )
86 38 60 84 85 70 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ∈ 𝐵 )
87 32 86 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ∈ 𝐵 )
88 difss ⊢ ( 𝐼 ∖ { 𝑌 } ) ⊆ 𝐼
89 3 88 eqsstri ⊢ 𝐽 ⊆ 𝐼
90 89 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝐽 ⊆ 𝐼 )
91 38 40 42 18 63 80 87 90 gsummptfsres ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
92 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ 𝐽 ) → 𝑖 ∈ 𝐽 )
93 92 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ 𝐽 ) → ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) = ( 𝑐 ‘ 𝑖 ) )
94 92 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ 𝐽 ) → ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
95 93 94 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑖 ∈ 𝐽 ) → ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) = ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) )
96 95 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) )
97 96 oveq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) )
98 91 97 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) )
99 36 98 oveq12d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) )
100 99 mpteq2dva ⊢ ( 𝜑 → ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) = ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ↦ ( ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) )
101 100 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ↦ ( ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) ) )
102 7 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
103 102 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
104 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
105 104 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
106 105 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
107 14 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) )
108 8 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → 𝐼 ∈ 𝑉 )
109 7 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → 𝑅 ∈ CRing )
110 9 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → 𝑌 ∈ 𝐼 )
111 10 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → 𝐹 ∈ 𝑀 )
112 difssd ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ⊆ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
113 112 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
114 16 17 108 109 110 3 4 111 113 extvfvv ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = if ( ( 𝑐 ‘ 𝑌 ) = 0 , ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) )
115 113 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
116 71 115 sselid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) )
117 22 115 elrabrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → 𝑐 finSupp 0 )
118 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → ( 𝑐 ‘ 𝑌 ) = 0 )
119 117 118 jca ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → ( 𝑐 finSupp 0 ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) )
120 28 116 119 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } )
121 simplr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) )
122 121 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → ¬ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } )
123 120 122 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ¬ ( 𝑐 ‘ 𝑌 ) = 0 )
124 123 iffalsed ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → if ( ( 𝑐 ‘ 𝑌 ) = 0 , ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
125 107 114 124 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
126 125 oveq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
127 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
128 102 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → 𝑅 ∈ Ring )
129 86 fmpttd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) : 𝐼 ⟶ 𝐵 )
130 38 40 82 67 129 79 gsumcl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ 𝐵 )
131 113 130 syldan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ 𝐵 )
132 5 127 17 128 131 ringlzd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
133 126 132 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∖ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ) → ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
134 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
135 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
136 16 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
137 16 17 8 102 5 3 4 9 10 135 extvfvcl ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
138 13 137 eqeltrid ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
139 134 5 135 136 138 mplelf ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ 𝐵 )
140 134 135 17 138 mplelsfi ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) finSupp ( 0g ‘ 𝑅 ) )
141 5 102 106 130 139 140 rmfsupp2 ⊢ ( 𝜑 → ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
142 102 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑅 ∈ Ring )
143 139 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ∈ 𝐵 )
144 5 127 142 143 130 ringcld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ∈ 𝐵 )
145 simpl ⊢ ( ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) → ℎ finSupp 0 )
146 145 a1i ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → ( ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) → ℎ finSupp 0 ) )
147 146 ss2rabdv ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
148 5 17 103 106 133 141 144 147 gsummptfsres ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
149 nfcv ⊢ Ⅎ 𝑏 ( ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) )
150 fveq2 ⊢ ( 𝑏 = ( 𝑐 ↾ 𝐽 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) )
151 fveq1 ⊢ ( 𝑏 = ( 𝑐 ↾ 𝐽 ) → ( 𝑏 ‘ 𝑖 ) = ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) )
152 151 oveq1d ⊢ ( 𝑏 = ( 𝑐 ↾ 𝐽 ) → ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) = ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) )
153 152 mpteq2dv ⊢ ( 𝑏 = ( 𝑐 ↾ 𝐽 ) → ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) )
154 153 oveq2d ⊢ ( 𝑏 = ( 𝑐 ↾ 𝐽 ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) = ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) )
155 150 154 oveq12d ⊢ ( 𝑏 = ( 𝑐 ↾ 𝐽 ) → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) = ( ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) )
156 ovex ⊢ ( ℕ0 ↑m 𝐽 ) ∈ V
157 156 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ∈ V
158 157 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ∈ V )
159 eqid ⊢ ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
160 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
161 160 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
162 159 5 4 161 10 mplelf ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ⟶ 𝐵 )
163 162 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑏 ) ) )
164 159 4 17 10 mplelsfi ⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
165 163 164 eqbrtrrd ⊢ ( 𝜑 → ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ↦ ( 𝐹 ‘ 𝑏 ) ) finSupp ( 0g ‘ 𝑅 ) )
166 102 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
167 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
168 5 127 17 166 167 ringlzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
169 162 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐵 )
170 81 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
171 89 a1i ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
172 8 171 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝐽 ∈ V )
174 170 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
175 174 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐽 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
176 ssrab2 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐽 )
177 176 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ0 ↑m 𝐽 ) )
178 177 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑏 ∈ ( ℕ0 ↑m 𝐽 ) )
179 178 elmaprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑏 : 𝐽 ⟶ ℕ0 )
180 179 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐽 ) → ( 𝑏 ‘ 𝑖 ) ∈ ℕ0 )
181 11 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝐴 : 𝐼 ⟶ 𝐵 )
182 89 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝐽 ⊆ 𝐼 )
183 181 182 fssresd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝐴 ↾ 𝐽 ) : 𝐽 ⟶ 𝐵 )
184 183 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐽 ) → ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ∈ 𝐵 )
185 38 60 175 180 184 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑖 ∈ 𝐽 ) → ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ∈ 𝐵 )
186 185 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) : 𝐽 ⟶ 𝐵 )
187 179 feqmptd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑏 = ( 𝑖 ∈ 𝐽 ↦ ( 𝑏 ‘ 𝑖 ) ) )
188 breq1 ⊢ ( ℎ = 𝑏 → ( ℎ finSupp 0 ↔ 𝑏 finSupp 0 ) )
189 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
190 188 189 elrabrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑏 finSupp 0 )
191 187 190 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑖 ∈ 𝐽 ↦ ( 𝑏 ‘ 𝑖 ) ) finSupp 0 )
192 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
193 fvexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 1r ‘ 𝑅 ) ∈ V )
194 191 192 180 184 193 fsuppssov1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) finSupp ( 1r ‘ 𝑅 ) )
195 38 40 170 173 186 194 gsumcl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ∈ 𝐵 )
196 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
197 165 168 169 195 196 fsuppssov1 ⊢ ( 𝜑 → ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
198 ssidd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
199 102 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑅 ∈ Ring )
200 5 127 199 169 195 ringcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ∈ 𝐵 )
201 breq1 ⊢ ( ℎ = ( 𝑐 ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( 𝑐 ↾ 𝐽 ) finSupp 0 ) )
202 25 90 elmapssresd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑐 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
203 65 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 0 ∈ ℕ0 )
204 31 203 fsuppres ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑐 ↾ 𝐽 ) finSupp 0 )
205 201 202 204 elrabd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑐 ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
206 breq1 ⊢ ( ℎ = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) → ( ℎ finSupp 0 ↔ ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) finSupp 0 ) )
207 fveq1 ⊢ ( ℎ = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) → ( ℎ ‘ 𝑌 ) = ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ‘ 𝑌 ) )
208 207 eqeq1d ⊢ ( ℎ = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) → ( ( ℎ ‘ 𝑌 ) = 0 ↔ ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ‘ 𝑌 ) = 0 ) )
209 206 208 anbi12d ⊢ ( ℎ = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) → ( ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) ↔ ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) finSupp 0 ∧ ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ‘ 𝑌 ) = 0 ) ) )
210 nn0ex ⊢ ℕ0 ∈ V
211 210 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ℕ0 ∈ V )
212 8 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
213 3 uneq1i ⊢ ( 𝐽 ∪ { 𝑌 } ) = ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } )
214 undifr ⊢ ( { 𝑌 } ⊆ 𝐼 ↔ ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
215 45 214 sylib ⊢ ( 𝜑 → ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
216 213 215 eqtrid ⊢ ( 𝜑 → ( 𝐽 ∪ { 𝑌 } ) = 𝐼 )
217 216 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝐽 ∪ { 𝑌 } ) = 𝐼 )
218 65 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
219 9 218 fsnd ⊢ ( 𝜑 → { ⟨ 𝑌 , 0 ⟩ } : { 𝑌 } ⟶ ℕ0 )
220 219 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → { ⟨ 𝑌 , 0 ⟩ } : { 𝑌 } ⟶ ℕ0 )
221 3 ineq1i ⊢ ( 𝐽 ∩ { 𝑌 } ) = ( ( 𝐼 ∖ { 𝑌 } ) ∩ { 𝑌 } )
222 disjdifr ⊢ ( ( 𝐼 ∖ { 𝑌 } ) ∩ { 𝑌 } ) = ∅
223 221 222 eqtri ⊢ ( 𝐽 ∩ { 𝑌 } ) = ∅
224 223 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝐽 ∩ { 𝑌 } ) = ∅ )
225 179 220 224 fun2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) : ( 𝐽 ∪ { 𝑌 } ) ⟶ ℕ0 )
226 217 225 feq2dd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) : 𝐼 ⟶ ℕ0 )
227 211 212 226 elmapdd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ∈ ( ℕ0 ↑m 𝐼 ) )
228 9 65 jctir ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0 ) )
229 228 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0 ) )
230 179 ffund ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → Fun 𝑏 )
231 neldifsnd ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝐼 ∖ { 𝑌 } ) )
232 3 eleq2i ⊢ ( 𝑌 ∈ 𝐽 ↔ 𝑌 ∈ ( 𝐼 ∖ { 𝑌 } ) )
233 231 232 sylnibr ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐽 )
234 233 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ¬ 𝑌 ∈ 𝐽 )
235 179 fdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → dom 𝑏 = 𝐽 )
236 234 235 neleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ¬ 𝑌 ∈ dom 𝑏 )
237 df-nel ⊢ ( 𝑌 ∉ dom 𝑏 ↔ ¬ 𝑌 ∈ dom 𝑏 )
238 236 237 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑌 ∉ dom 𝑏 )
239 230 238 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏 ) )
240 funsnfsupp ⊢ ( ( ( 𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0 ) ∧ ( Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏 ) ) → ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) finSupp 0 ↔ 𝑏 finSupp 0 ) )
241 240 biimpar ⊢ ( ( ( ( 𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0 ) ∧ ( Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏 ) ) ∧ 𝑏 finSupp 0 ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) finSupp 0 )
242 229 239 190 241 syl21anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) finSupp 0 )
243 9 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 𝑌 ∈ 𝐼 )
244 65 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ0 )
245 fsnunfv ⊢ ( ( 𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0 ∧ ¬ 𝑌 ∈ dom 𝑏 ) → ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ‘ 𝑌 ) = 0 )
246 243 244 236 245 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ‘ 𝑌 ) = 0 )
247 242 246 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) finSupp 0 ∧ ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ‘ 𝑌 ) = 0 ) )
248 209 227 247 elrabd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } )
249 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → 𝑏 = ( 𝑐 ↾ 𝐽 ) )
250 249 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) = ( ( 𝑐 ↾ 𝐽 ) ∪ { ⟨ 𝑌 , 0 ⟩ } ) )
251 3 reseq2i ⊢ ( 𝑐 ↾ 𝐽 ) = ( 𝑐 ↾ ( 𝐼 ∖ { 𝑌 } ) )
252 251 uneq1i ⊢ ( ( 𝑐 ↾ 𝐽 ) ∪ { ⟨ 𝑌 , 0 ⟩ } ) = ( ( 𝑐 ↾ ( 𝐼 ∖ { 𝑌 } ) ) ∪ { ⟨ 𝑌 , 0 ⟩ } )
253 252 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → ( ( 𝑐 ↾ 𝐽 ) ∪ { ⟨ 𝑌 , 0 ⟩ } ) = ( ( 𝑐 ↾ ( 𝐼 ∖ { 𝑌 } ) ) ∪ { ⟨ 𝑌 , 0 ⟩ } ) )
254 25 elmaprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → 𝑐 : 𝐼 ⟶ ℕ0 )
255 254 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → 𝑐 : 𝐼 ⟶ ℕ0 )
256 255 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → 𝑐 Fn 𝐼 )
257 243 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → 𝑌 ∈ 𝐼 )
258 30 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → ( 𝑐 finSupp 0 ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) )
259 258 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → ( 𝑐 ‘ 𝑌 ) = 0 )
260 fresunsn ⊢ ( ( 𝑐 Fn 𝐼 ∧ 𝑌 ∈ 𝐼 ∧ ( 𝑐 ‘ 𝑌 ) = 0 ) → ( ( 𝑐 ↾ ( 𝐼 ∖ { 𝑌 } ) ) ∪ { ⟨ 𝑌 , 0 ⟩ } ) = 𝑐 )
261 256 257 259 260 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → ( ( 𝑐 ↾ ( 𝐼 ∖ { 𝑌 } ) ) ∪ { ⟨ 𝑌 , 0 ⟩ } ) = 𝑐 )
262 250 253 261 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑏 = ( 𝑐 ↾ 𝐽 ) ) → 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) )
263 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) )
264 263 reseq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → ( 𝑐 ↾ 𝐽 ) = ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ↾ 𝐽 ) )
265 179 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → 𝑏 : 𝐽 ⟶ ℕ0 )
266 265 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → 𝑏 Fn 𝐽 )
267 234 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → ¬ 𝑌 ∈ 𝐽 )
268 fsnunres ⊢ ( ( 𝑏 Fn 𝐽 ∧ ¬ 𝑌 ∈ 𝐽 ) → ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ↾ 𝐽 ) = 𝑏 )
269 266 267 268 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → ( ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ↾ 𝐽 ) = 𝑏 )
270 264 269 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) ∧ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) → 𝑏 = ( 𝑐 ↾ 𝐽 ) )
271 262 270 impbida ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) ∧ 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ) → ( 𝑏 = ( 𝑐 ↾ 𝐽 ) ↔ 𝑐 = ( 𝑏 ∪ { ⟨ 𝑌 , 0 ⟩ } ) ) )
272 248 271 reu6dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ) → ∃! 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } 𝑏 = ( 𝑐 ↾ 𝐽 ) )
273 149 5 17 155 103 158 197 198 200 205 272 gsummptfsf1o ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ℎ finSupp 0 ∧ ( ℎ ‘ 𝑌 ) = 0 ) } ↦ ( ( 𝐹 ‘ ( 𝑐 ↾ 𝐽 ) ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( ( 𝑐 ↾ 𝐽 ) ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) ) )
274 101 148 273 3eqtr4d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) ) )
275 1 5 evlval ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 )
276 eqid ⊢ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) )
277 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) )
278 eqid ⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
279 5 subrgid ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
280 102 279 syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
281 5 ressid ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
282 7 281 syl ⊢ ( 𝜑 → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
283 282 oveq2d ⊢ ( 𝜑 → ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐼 mPoly 𝑅 ) )
284 283 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
285 138 284 eleqtrrd ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) ) )
286 5 fvexi ⊢ 𝐵 ∈ V
287 286 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
288 287 8 11 elmapdd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑m 𝐼 ) )
289 275 276 277 278 136 5 37 60 127 8 7 280 285 288 evlsvvval ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ) ‘ 𝐴 ) = ( 𝑅 Σg ( 𝑐 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ‘ 𝑐 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑐 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
290 2 5 evlval ⊢ 𝑂 = ( ( 𝐽 evalSub 𝑅 ) ‘ 𝐵 )
291 eqid ⊢ ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) )
292 eqid ⊢ ( Base ‘ ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( Base ‘ ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) ) )
293 10 4 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
294 282 oveq2d ⊢ ( 𝜑 → ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐽 mPoly 𝑅 ) )
295 294 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
296 293 295 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐽 mPoly ( 𝑅 ↾s 𝐵 ) ) ) )
297 288 171 elmapssresd ⊢ ( 𝜑 → ( 𝐴 ↾ 𝐽 ) ∈ ( 𝐵 ↑m 𝐽 ) )
298 290 291 292 278 161 5 37 60 127 172 7 280 296 297 evlsvvval ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐴 ↾ 𝐽 ) ) = ( 𝑅 Σg ( 𝑏 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑖 ∈ 𝐽 ↦ ( ( 𝑏 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) ( ( 𝐴 ↾ 𝐽 ) ‘ 𝑖 ) ) ) ) ) ) ) )
299 274 289 298 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐸 ‘ 𝑌 ) ‘ 𝐹 ) ) ‘ 𝐴 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐴 ↾ 𝐽 ) ) )