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

Metamath Proof Explorer

Theorem 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 = ( 0g ‘ 𝑊 )
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 = ( 0g ‘ 𝑊 )
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 ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
49 1 2 4 48 3 slmd0vs ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑄 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) · 𝑄 ) = 0 )
50 8 9 49 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝐺 ) · 𝑄 ) = 0 )
51 50 eqcomd ⊢ ( 𝜑 → 0 = ( ( 0g ‘ 𝐺 ) · 𝑄 ) )
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 ∅ ) = ( 0g ‘ 𝐺 )
59 57 58 eqtri ⊢ ( 𝐺 Σg ( 𝑘 ∈ ∅ ↦ 𝑃 ) ) = ( 0g ‘ 𝐺 )
60 59 oveq1i ⊢ ( ( 𝐺 Σg ( 𝑘 ∈ ∅ ↦ 𝑃 ) ) · 𝑄 ) = ( ( 0g ‘ 𝐺 ) · 𝑄 )
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 ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 0g ‘ 𝐺 ) ∈ V )
87 83 84 85 86 fsuppmptdm ⊢ ( ( ( 𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒 ) ∧ ( 𝜑 ∧ ( 𝑒 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑘 ∈ 𝑒 ↦ 𝑃 ) finSupp ( 0g ‘ 𝐺 ) )
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 ( 𝑘 ∈ 𝐴 ↦ 𝑃 ) ) · 𝑄 ) )