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