Metamath Proof Explorer


Theorem 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 = ( 0g𝑊 )
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 = ( 0g𝑊 )
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 ( 𝑘𝐴𝑄 ) ) ) )