gsumvsca2

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

	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 )
	gsumvsca2.n	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
	gsumvsca2.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐾 )
Assertion	gsumvsca2	⊢ ( 𝜑 → ( 𝑊 Σ_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		gsumvsca2.n	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
10		gsumvsca2.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐾 )
11		ssid	⊢ 𝐴 ⊆ 𝐴
12		sseq1	⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
13	12	anbi2d	⊢ ( 𝑎 = ∅ → ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ ∅ ⊆ 𝐴 ) ) )
14		mpteq1	⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) = ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) )
15	14	oveq2d	⊢ ( 𝑎 = ∅ → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) )
16		mpteq1	⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ 𝑃 ) = ( 𝑘 ∈ ∅ ↦ 𝑃 ) )
17	16	oveq2d	⊢ ( 𝑎 = ∅ → ( 𝐺 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑃 ) ) = ( 𝐺 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑃 ) ) )
18	17	oveq1d	⊢ ( 𝑎 = ∅ → ( ( 𝐺 Σ_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	oveq1d	⊢ ( 𝑎 = 𝑒 → ( ( 𝐺 Σ_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	oveq1d	⊢ ( 𝑎 = ( 𝑒 ∪ { 𝑧 } ) → ( ( 𝐺 Σ_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	oveq1d	⊢ ( 𝑎 = 𝐴 → ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑃 ) ) · 𝑄 ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) )
46	42 45	eqeq12d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑃 ) ) · 𝑄 ) ↔ ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) ) )
47	40 46	imbi12d	⊢ ( 𝑎 = 𝐴 → ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑎 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑎 ↦ 𝑃 ) ) · 𝑄 ) ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) ) ) )
48		eqid	⊢ ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐺 )
49	1 2 4 48 3	slmd0vs	⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑄 ∈ 𝐵 ) → ( ( 0_g ‘ 𝐺 ) · 𝑄 ) = 0 )
50	8 9 49	syl2anc	⊢ ( 𝜑 → ( ( 0_g ‘ 𝐺 ) · 𝑄 ) = 0 )
51	50	eqcomd	⊢ ( 𝜑 → 0 = ( ( 0_g ‘ 𝐺 ) · 𝑄 ) )
52		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) = ∅
53	52	oveq2i	⊢ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = ( 𝑊 Σ_g ∅ )
54	3	gsum0	⊢ ( 𝑊 Σ_g ∅ ) = 0
55	53 54	eqtri	⊢ ( 𝑊 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝑃 · 𝑄 ) ) ) = 0
56		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ 𝑃 ) = ∅
57	56	oveq2i	⊢ ( 𝐺 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑃 ) ) = ( 𝐺 Σ_g ∅ )
58	48	gsum0	⊢ ( 𝐺 Σ_g ∅ ) = ( 0_g ‘ 𝐺 )
59	57 58	eqtri	⊢ ( 𝐺 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑃 ) ) = ( 0_g ‘ 𝐺 )
60	59	oveq1i	⊢ ( ( 𝐺 Σ_g ( 𝑘 ∈ ∅ ↦ 𝑃 ) ) · 𝑄 ) = ( ( 0_g ‘ 𝐺 ) · 𝑄 )
61	51 55 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		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
70	2	slmdsrg	⊢ ( 𝑊 ∈ SLMod → 𝐺 ∈ SRing )
71		srgcmn	⊢ ( 𝐺 ∈ SRing → 𝐺 ∈ CMnd )
72	68 70 71	3syl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝐺 ∈ CMnd )
73		vex	⊢ 𝑒 ∈ V
74	73	a1i	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑒 ∈ V )
75		simplrl	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝜑 )
76		simprr	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 )
77	76	unssad	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑒 ⊆ 𝐴 )
78	77	sselda	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑘 ∈ 𝐴 )
79	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐾 ⊆ ( Base ‘ 𝐺 ) )
80	79 10	sseldd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐺 ) )
81	75 78 80	syl2anc	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑃 ∈ ( Base ‘ 𝐺 ) )
82	81	fmpttd	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) : 𝑒 ⟶ ( Base ‘ 𝐺 ) )
83		eqid	⊢ ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) = ( 𝑘 ∈ 𝑒 ↦ 𝑃 )
84		simpll	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑒 ∈ Fin )
85	75 78 10	syl2anc	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑃 ∈ 𝐾 )
86		fvexd	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 0_g ‘ 𝐺 ) ∈ V )
87	83 84 85 86	fsuppmptdm	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) finSupp ( 0_g ‘ 𝐺 ) )
88	69 48 72 74 82 87	gsumcl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ∈ ( Base ‘ 𝐺 ) )
89	76	unssbd	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → { 𝑧 } ⊆ 𝐴 )
90		vex	⊢ 𝑧 ∈ V
91	90	snss	⊢ ( 𝑧 ∈ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 )
92	89 91	sylibr	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
93	80	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑃 ∈ ( Base ‘ 𝐺 ) )
94	93	ad2antrl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ∀ 𝑘 ∈ 𝐴 𝑃 ∈ ( Base ‘ 𝐺 ) )
95		rspcsbela	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝑃 ∈ ( Base ‘ 𝐺 ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ∈ ( Base ‘ 𝐺 ) )
96	92 94 95	syl2anc	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ∈ ( Base ‘ 𝐺 ) )
97	9	ad2antrl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
98		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
99	1 5 2 4 69 98	slmdvsdir	⊢ ( ( 𝑊 ∈ SLMod ∧ ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ∈ ( Base ‘ 𝐺 ) ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ 𝑄 ∈ 𝐵 ) ) → ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ( +_g ‘ 𝐺 ) ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ) · 𝑄 ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
100	68 88 96 97 99	syl13anc	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ( +_g ‘ 𝐺 ) ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ) · 𝑄 ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
101	100	adantr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ( +_g ‘ 𝐺 ) ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ) · 𝑄 ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
102		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝑃
103	90	a1i	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ V )
104		simplr	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ¬ 𝑧 ∈ 𝑒 )
105		csbeq1a	⊢ ( 𝑘 = 𝑧 → 𝑃 = ⦋ 𝑧 / 𝑘 ⦌ 𝑃 )
106	102 69 98 72 84 81 103 104 96 105	gsumunsnf	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ( +_g ‘ 𝐺 ) ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ) )
107	106	oveq1d	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) · 𝑄 ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ( +_g ‘ 𝐺 ) ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ) · 𝑄 ) )
108	107	adantr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) · 𝑄 ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) ( +_g ‘ 𝐺 ) ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ) · 𝑄 ) )
109		nfcv	⊢ Ⅎ 𝑘 ·
110		nfcv	⊢ Ⅎ 𝑘 𝑄
111	102 109 110	nfov	⊢ Ⅎ 𝑘 ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 )
112		slmdcmn	⊢ ( 𝑊 ∈ SLMod → 𝑊 ∈ CMnd )
113	68 112	syl	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑊 ∈ CMnd )
114	75 8	syl	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑊 ∈ SLMod )
115	75 9	syl	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → 𝑄 ∈ 𝐵 )
116	1 2 4 69	slmdvscl	⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 · 𝑄 ) ∈ 𝐵 )
117	114 81 115 116	syl3anc	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ 𝑘 ∈ 𝑒 ) → ( 𝑃 · 𝑄 ) ∈ 𝐵 )
118	1 2 4 69	slmdvscl	⊢ ( ( 𝑊 ∈ SLMod ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝑃 ∈ ( Base ‘ 𝐺 ) ∧ 𝑄 ∈ 𝐵 ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ∈ 𝐵 )
119	68 96 97 118	syl3anc	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ∈ 𝐵 )
120	105	oveq1d	⊢ ( 𝑘 = 𝑧 → ( 𝑃 · 𝑄 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) )
121	111 1 5 113 84 117 103 104 119 120	gsumunsnf	⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
122	121	adantr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
123		simpr	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) )
124	123	oveq1d	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
125	122 124	eqtrd	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) + ( ⦋ 𝑧 / 𝑘 ⦌ 𝑃 · 𝑄 ) ) )
126	101 108 125	3eqtr4rd	⊢ ( ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) ∧ ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) · 𝑄 ) )
127	126	exp31	⊢ ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) · 𝑄 ) ) ) )
128	127	a2d	⊢ ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) → ( ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) · 𝑄 ) ) ) )
129	67 128	syl5	⊢ ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) → ( ( ( 𝜑 ∧ 𝑒 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝑒 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) ) · 𝑄 ) ) → ( ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝑒 ∪ { 𝑧 } ) ↦ 𝑃 ) ) · 𝑄 ) ) ) )
130	20 29 38 47 62 129	findcard2s	⊢ ( 𝐴 ∈ Fin → ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) ) )
131	130	imp	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) )
132	11 131	mpanr2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝜑 ) → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) )
133	7 132	mpancom	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑘 ∈ 𝐴 ↦ ( 𝑃 · 𝑄 ) ) ) = ( ( 𝐺 Σ_g ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) )

Metamath Proof Explorer

Theorem gsumvsca2

Proof