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

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