gsumvsca1

Description: Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018)

	Ref	Expression
Hypotheses	gsumvsca.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	gsumvsca.g	⊢ 𝐺 = ( Scalar ‘ 𝑊 )
	gsumvsca.z	⊢ 0 = ( 0_g ‘ 𝑊 )
	gsumvsca.t	⊢ · = ( ·_𝑠 ‘ 𝑊 )
	gsumvsca.p	⊢ + = ( +_g ‘ 𝑊 )
	gsumvsca.k	⊢ ( 𝜑 → 𝐾 ⊆ ( Base ‘ 𝐺 ) )
	gsumvsca.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsumvsca.w	⊢ ( 𝜑 → 𝑊 ∈ SLMod )
	gsumvsca1.n	⊢ ( 𝜑 → 𝑃 ∈ 𝐾 )
	gsumvsca1.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑄 ∈ 𝐵 )
Assertion	gsumvsca1	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumvsca.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		gsumvsca.g	⊢ 𝐺 = ( Scalar ‘ 𝑊 )
3		gsumvsca.z	⊢ 0 = ( 0_g ‘ 𝑊 )
4		gsumvsca.t	⊢ · = ( ·_𝑠 ‘ 𝑊 )
5		gsumvsca.p	⊢ + = ( +_g ‘ 𝑊 )
6		gsumvsca.k	⊢ ( 𝜑 → 𝐾 ⊆ ( Base ‘ 𝐺 ) )
7		gsumvsca.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
8		gsumvsca.w	⊢ ( 𝜑 → 𝑊 ∈ SLMod )
9		gsumvsca1.n	⊢ ( 𝜑 → 𝑃 ∈ 𝐾 )
10		gsumvsca1.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑄 ∈ 𝐵 )
11		ssid	⊢ 𝐴 ⊆ 𝐴
12		sseq1	⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
13	12	anbi2d	⊢ ( 𝑎 = ∅ → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ ∅ ⊆ 𝐴 ) ) )
14		mpteq1	⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) = ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) )
15	14	oveq2d	⊢ ( 𝑎 = ∅ → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) )
16		mpteq1	⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) = ( 𝑘 ∈ ∅ ↦ 𝑄 ) )
17	16	oveq2d	⊢ ( 𝑎 = ∅ → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) )
18	17	oveq2d	⊢ ( 𝑎 = ∅ → ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) ) )
19	15 18	eqeq12d	⊢ ( 𝑎 = ∅ → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ↔ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) ) ) )
20	13 19	imbi12d	⊢ ( 𝑎 = ∅ → ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ) ↔ ( ( 𝜑 ∧ ∅ ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) ) ) ) )
21		sseq1	⊢ ( 𝑎 = 𝑒 → ( 𝑎 ⊆ 𝐴 ↔ 𝑒 ⊆ 𝐴 ) )
22	21	anbi2d	⊢ ( 𝑎 = 𝑒 → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝑒 ⊆ 𝐴 ) ) )
23		mpteq1	⊢ ( 𝑎 = 𝑒 → ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) = ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) )
24	23	oveq2d	⊢ ( 𝑎 = 𝑒 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) )
25		mpteq1	⊢ ( 𝑎 = 𝑒 → ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) = ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) )
26	25	oveq2d	⊢ ( 𝑎 = 𝑒 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) )
27	26	oveq2d	⊢ ( 𝑎 = 𝑒 → ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) )
28	24 27	eqeq12d	⊢ ( 𝑎 = 𝑒 → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ↔ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) )
29	22 28	imbi12d	⊢ ( 𝑎 = 𝑒 → ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑒 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) ) )
30		sseq1	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( 𝑎 ⊆ 𝐴 ↔ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
31	30	anbi2d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) )
32		mpteq1	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) = ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) )
33	32	oveq2d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) )
34		mpteq1	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) = ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) )
35	34	oveq2d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) )
36	35	oveq2d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) )
37	33 36	eqeq12d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ↔ ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) ) )
38	31 37	imbi12d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) ) ) )
39		sseq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
40	39	anbi2d	⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) ) )
41		mpteq1	⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) )
42	41	oveq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) )
43		mpteq1	⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) )
44	43	oveq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) )
45	44	oveq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) )
46	42 45	eqeq12d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ↔ ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) ) )
47	40 46	imbi12d	⊢ ( 𝑎 = 𝐴 → ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑄 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) ) ) )
48	6 9	sseldd	⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐺 ) )
49		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
50	2 4 49 3	slmdvs0	⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑃 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑃 · 0 ) = 0 )
51	8 48 50	syl2anc	⊢ ( 𝜑 → ( 𝑃 · 0 ) = 0 )
52	51	eqcomd	⊢ ( 𝜑 → 0 = ( 𝑃 · 0 ) )
53		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) = ∅
54	53	oveq2i	⊢ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ∅ )
55	3	gsum0	⊢ ( 𝑊 Σ_g ∅ ) = 0
56	54 55	eqtri	⊢ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = 0
57		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ 𝑄 ) = ∅
58	57	oveq2i	⊢ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) = ( 𝑊 Σ_g ∅ )
59	58 55	eqtri	⊢ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) = 0
60	59	oveq2i	⊢ ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) ) = ( 𝑃 · 0 )
61	52 56 60	3eqtr4g	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) ) )
62	61	adantr	⊢ ( ( 𝜑 ∧ ∅ ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑄 ) ) ) )
63		ssun1	⊢ 𝑒 ⊆ ( 𝑒 ∪ { 𝑧 } )
64		sstr2	⊢ ( 𝑒 ⊆ ( 𝑒 ∪ { 𝑧 } ) → ( ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑒 ⊆ 𝐴 ) )
65	63 64	ax-mp	⊢ ( ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑒 ⊆ 𝐴 )
66	65	anim2i	⊢ ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝜑 ∧ 𝑒 ⊆ 𝐴 ) )
67	66	imim1i	⊢ ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) )
68	8	ad2antrl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑊 ∈ SLMod )
69	48	ad2antrl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐺 ) )
70		slmdcmn	⊢ ( 𝑊 ∈ SLMod → 𝑊 ∈ CMnd )
71	68 70	syl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑊 ∈ CMnd )
72		vex	⊢ 𝑒 ∈ V
73	72	a1i	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑒 ∈ V )
74		simplrl	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝜑 )
75		simprr	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 )
76	75	unssad	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑒 ⊆ 𝐴 )
77	76	sselda	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑘 ∈ 𝐴 )
78	74 77 10	syl2anc	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑄 ∈ 𝐵 )
79	78	fmpttd	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) : 𝑒 ⟶ 𝐵 )
80		eqid	⊢ ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) = ( 𝑘 ∈ 𝑒 ↦ 𝑄 )
81		simpll	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑒 ∈ Fin )
82	3	fvexi	⊢ 0 ∈ V
83	82	a1i	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 0 ∈ V )
84	80 81 78 83	fsuppmptdm	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) finSupp 0 )
85	1 3 71 73 79 84	gsumcl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ∈ 𝐵 )
86	75	unssbd	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → { 𝑧 } ⊆ 𝐴 )
87		vex	⊢ 𝑧 ∈ V
88	87	snss	⊢ ( 𝑧 ∈ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 )
89	86 88	sylibr	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
90	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑄 ∈ 𝐵 )
91	90	ad2antrl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ∀ 𝑘 ∈ 𝐴 𝑄 ∈ 𝐵 )
92		rspcsbela	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝑄 ∈ 𝐵 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ∈ 𝐵 )
93	89 91 92	syl2anc	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ∈ 𝐵 )
94	1 5 2 4 49	slmdvsdi	⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ∈ 𝐵 ) ) → ( 𝑃 · ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) + ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) = ( ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
95	68 69 85 93 94	syl13anc	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑃 · ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) + ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) = ( ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
96	95	adantr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( 𝑃 · ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) + ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) = ( ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
97		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝑄
98	87	a1i	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ V )
99		simplr	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ¬ 𝑧 ∈ 𝑒 )
100		csbeq1a	⊢ ( 𝑘 = 𝑧 → 𝑄 = ⦋ 𝑧 / 𝑘 ⦌ 𝑄 )
101	97 1 5 71 81 78 98 99 93 100	gsumunsnf	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) = ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) + ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) )
102	101	oveq2d	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) = ( 𝑃 · ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) + ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
103	102	adantr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) = ( 𝑃 · ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) + ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
104		nfcv	⊢ Ⅎ 𝑘 𝑃
105		nfcv	⊢ Ⅎ 𝑘 ·
106	104 105 97	nfov	⊢ Ⅎ 𝑘 ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 )
107	74 8	syl	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑊 ∈ SLMod )
108	74 48	syl	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑃 ∈ ( Base ‘ 𝐺 ) )
109	1 2 4 49	slmdvscl	⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 · 𝑄 ) ∈ 𝐵 )
110	107 108 78 109	syl3anc	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → ( 𝑃 · 𝑄 ) ∈ 𝐵 )
111	1 2 4 49	slmdvscl	⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ∈ 𝐵 ) → ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ∈ 𝐵 )
112	68 69 93 111	syl3anc	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ∈ 𝐵 )
113	100	oveq2d	⊢ ( 𝑘 = 𝑧 → ( 𝑃 · 𝑄 ) = ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) )
114	106 1 5 71 81 110 98 99 112 113	gsumunsnf	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
115	114	adantr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
116		simpr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) )
117	116	oveq1d	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) = ( ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
118	115 117	eqtrd	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) + ( 𝑃 · ⦋ 𝑧 / 𝑘 ⦌ 𝑄 ) ) )
119	96 103 118	3eqtr4rd	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) )
120	119	exp31	⊢ ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) ) ) )
121	120	a2d	⊢ ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) → ( ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) ) ) )
122	67 121	syl5	⊢ ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) → ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑄 ) ) ) ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑄 ) ) ) ) ) )
123	20 29 38 47 62 122	findcard2s	⊢ ( 𝐴 ∈ Fin → ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) ) )
124	123	imp	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) )
125	11 124	mpanr2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝜑 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) )
126	7 125	mpancom	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑃 · ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑄 ) ) ) )

Metamath Proof Explorer

Theorem gsumvsca1

Proof