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