evlsbagval

Description: Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since .0. and .1. using U instead of S may not be convenient. (Contributed by SN, 29-Jul-2024)

	Ref	Expression
Hypotheses	evlsbagval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsbagval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
	evlsbagval.u	⊢ 𝑈 = ( 𝑆 ↾_s 𝑅 )
	evlsbagval.w	⊢ 𝑊 = ( Base ‘ 𝑃 )
	evlsbagval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsbagval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
	evlsbagval.e	⊢ ↑ = ( ._g ‘ 𝑀 )
	evlsbagval.z	⊢ 0 = ( 0_g ‘ 𝑈 )
	evlsbagval.o	⊢ 1 = ( 1_r ‘ 𝑈 )
	evlsbagval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
	evlsbagval.f	⊢ 𝐹 = ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝐵 , 1 , 0 ) )
	evlsbagval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsbagval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsbagval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsbagval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑_m 𝐼 ) )
	evlsbagval.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion	evlsbagval	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsbagval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsbagval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsbagval.u	⊢ 𝑈 = ( 𝑆 ↾_s 𝑅 )
4		evlsbagval.w	⊢ 𝑊 = ( Base ‘ 𝑃 )
5		evlsbagval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		evlsbagval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
7		evlsbagval.e	⊢ ↑ = ( ._g ‘ 𝑀 )
8		evlsbagval.z	⊢ 0 = ( 0_g ‘ 𝑈 )
9		evlsbagval.o	⊢ 1 = ( 1_r ‘ 𝑈 )
10		evlsbagval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
11		evlsbagval.f	⊢ 𝐹 = ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝐵 , 1 , 0 ) )
12		evlsbagval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
13		evlsbagval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
14		evlsbagval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
15		evlsbagval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑_m 𝐼 ) )
16		evlsbagval.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
17		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ∈ V )
18		ovexd	⊢ ( 𝜑 → ( ℕ₀ ↑_m 𝐼 ) ∈ V )
19	10 18	rabexd	⊢ ( 𝜑 → 𝐷 ∈ V )
20	3	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
21	14 20	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
22		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
23	22 9	ringidcl	⊢ ( 𝑈 ∈ Ring → 1 ∈ ( Base ‘ 𝑈 ) )
24	21 23	syl	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑈 ) )
25	22 8	ring0cl	⊢ ( 𝑈 ∈ Ring → 0 ∈ ( Base ‘ 𝑈 ) )
26	21 25	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑈 ) )
27	24 26	ifcld	⊢ ( 𝜑 → if ( 𝑠 = 𝐵 , 1 , 0 ) ∈ ( Base ‘ 𝑈 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐷 ) → if ( 𝑠 = 𝐵 , 1 , 0 ) ∈ ( Base ‘ 𝑈 ) )
29	28 11	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) )
30	17 19 29	elmapdd	⊢ ( 𝜑 → 𝐹 ∈ ( ( Base ‘ 𝑈 ) ↑_m 𝐷 ) )
31		eqid	⊢ ( 𝐼 mPwSer 𝑈 ) = ( 𝐼 mPwSer 𝑈 )
32		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑈 ) )
33	31 22 10 32 12	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) = ( ( Base ‘ 𝑈 ) ↑_m 𝐷 ) )
34	30 33	eleqtrrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) )
35	19 26 11	sniffsupp	⊢ ( 𝜑 → 𝐹 finSupp 0 )
36	2 31 32 8 4	mplelbas	⊢ ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) ∧ 𝐹 finSupp 0 ) )
37	34 35 36	sylanbrc	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
38		eqid	⊢ ( ._r ‘ 𝑆 ) = ( ._r ‘ 𝑆 )
39	1 2 4 3 10 5 6 7 38 12 13 14 37 15	evlsvvval	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σ_g ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) )
40	16	snssd	⊢ ( 𝜑 → { 𝐵 } ⊆ 𝐷 )
41		resmpt	⊢ ( { 𝐵 } ⊆ 𝐷 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) = ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
42	40 41	syl	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) = ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
43	42	oveq2d	⊢ ( 𝜑 → ( 𝑆 Σ_g ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) ) = ( 𝑆 Σ_g ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) )
44		eqid	⊢ ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑆 )
45	13	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
46	45	ringcmnd	⊢ ( 𝜑 → 𝑆 ∈ CMnd )
47	45	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring )
48	3	subrgbas	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
49	5	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
50	48 49	eqsstrrd	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
51	14 50	syl	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
52	29 51	fssd	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐾 )
53	52	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 )
54	12	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
55	13	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing )
56	15	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐾 ↑_m 𝐼 ) )
57		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
58	10 5 6 7 54 55 56 57	evlsvvvallem	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
59	5 38 47 53 58	ringcld	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ∈ 𝐾 )
60	59	fmpttd	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) : 𝐷 ⟶ 𝐾 )
61		eldifsnneq	⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) → ¬ 𝑏 = 𝐵 )
62	61	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ¬ 𝑏 = 𝐵 )
63	62	iffalsed	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → if ( 𝑏 = 𝐵 , 1 , 0 ) = 0 )
64		eqeq1	⊢ ( 𝑠 = 𝑏 → ( 𝑠 = 𝐵 ↔ 𝑏 = 𝐵 ) )
65	64	ifbid	⊢ ( 𝑠 = 𝑏 → if ( 𝑠 = 𝐵 , 1 , 0 ) = if ( 𝑏 = 𝐵 , 1 , 0 ) )
66		eldifi	⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) → 𝑏 ∈ 𝐷 )
67	66	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → 𝑏 ∈ 𝐷 )
68	9	fvexi	⊢ 1 ∈ V
69	8	fvexi	⊢ 0 ∈ V
70	68 69	ifex	⊢ if ( 𝑏 = 𝐵 , 1 , 0 ) ∈ V
71	70	a1i	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → if ( 𝑏 = 𝐵 , 1 , 0 ) ∈ V )
72	11 65 67 71	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑏 ) = if ( 𝑏 = 𝐵 , 1 , 0 ) )
73	3 44	subrg0	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑈 ) )
74	73 8	eqtr4di	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0_g ‘ 𝑆 ) = 0 )
75	14 74	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑆 ) = 0 )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 0_g ‘ 𝑆 ) = 0 )
77	63 72 76	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0_g ‘ 𝑆 ) )
78	77	oveq1d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 0_g ‘ 𝑆 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
79	66 58	sylan2	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
80	5 38 44	ringlz	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 ) → ( ( 0_g ‘ 𝑆 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0_g ‘ 𝑆 ) )
81	45 79 80	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 0_g ‘ 𝑆 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0_g ‘ 𝑆 ) )
82	78 81	eqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 0_g ‘ 𝑆 ) )
83	82 19	suppss2	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) supp ( 0_g ‘ 𝑆 ) ) ⊆ { 𝐵 } )
84	10 2 3 4 5 6 7 38 12 13 14 37 15	evlsvvvallem2	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) finSupp ( 0_g ‘ 𝑆 ) )
85	5 44 46 19 60 83 84	gsumres	⊢ ( 𝜑 → ( 𝑆 Σ_g ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ↾ { 𝐵 } ) ) = ( 𝑆 Σ_g ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) )
86	13	crnggrpd	⊢ ( 𝜑 → 𝑆 ∈ Grp )
87	86	grpmndd	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
88	52 16	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ 𝐾 )
89	10 5 6 7 12 13 15 16	evlsvvvallem	⊢ ( 𝜑 → ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
90	5 38 45 88 89	ringcld	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ∈ 𝐾 )
91		fveq2	⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
92		fveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑣 ) = ( 𝐵 ‘ 𝑣 ) )
93	92	oveq1d	⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) = ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) )
94	93	mpteq2dv	⊢ ( 𝑏 = 𝐵 → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
95	94	oveq2d	⊢ ( 𝑏 = 𝐵 → ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
96	91 95	oveq12d	⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝐹 ‘ 𝐵 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
97	5 96	gsumsn	⊢ ( ( 𝑆 ∈ Mnd ∧ 𝐵 ∈ 𝐷 ∧ ( ( 𝐹 ‘ 𝐵 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ∈ 𝐾 ) → ( 𝑆 Σ_g ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( ( 𝐹 ‘ 𝐵 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
98	87 16 90 97	syl3anc	⊢ ( 𝜑 → ( 𝑆 Σ_g ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( ( 𝐹 ‘ 𝐵 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
99		iftrue	⊢ ( 𝑠 = 𝐵 → if ( 𝑠 = 𝐵 , 1 , 0 ) = 1 )
100	68	a1i	⊢ ( 𝜑 → 1 ∈ V )
101	11 99 16 100	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = 1 )
102		eqid	⊢ ( 1_r ‘ 𝑆 ) = ( 1_r ‘ 𝑆 )
103	3 102	subrg1	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 1_r ‘ 𝑆 ) = ( 1_r ‘ 𝑈 ) )
104	14 103	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑆 ) = ( 1_r ‘ 𝑈 ) )
105	9 101 104	3eqtr4a	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = ( 1_r ‘ 𝑆 ) )
106	105	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 1_r ‘ 𝑆 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
107	5 38 102 45 89	ringlidmd	⊢ ( 𝜑 → ( ( 1_r ‘ 𝑆 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
108	98 106 107	3eqtrd	⊢ ( 𝜑 → ( 𝑆 Σ_g ( 𝑏 ∈ { 𝐵 } ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
109	43 85 108	3eqtr3d	⊢ ( 𝜑 → ( 𝑆 Σ_g ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) ( ._r ‘ 𝑆 ) ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
110	39 109	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
111	37 110	jca	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ∧ ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑀 Σ_g ( 𝑣 ∈ 𝐼 ↦ ( ( 𝐵 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )

Metamath Proof Explorer

Theorem evlsbagval

Proof