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 ( 𝑘𝐴𝑃 ) ) · 𝑄 ) )