Step | Hyp | Ref
| Expression |
1 | | gsumvsca.a |
. 2
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | ssid 3587 |
. . 3
⊢ 𝐴 ⊆ 𝐴 |
3 | | sseq1 3589 |
. . . . . . 7
⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
4 | 3 | anbi2d 736 |
. . . . . 6
⊢ (𝑎 = ∅ → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴))) |
5 | | mpteq1 4665 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄)) = (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄))) |
6 | 5 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = ∅ → (𝑊 Σg
(𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑊 Σg (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄)))) |
7 | | mpteq1 4665 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝑘 ∈ 𝑎 ↦ 𝑄) = (𝑘 ∈ ∅ ↦ 𝑄)) |
8 | 7 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = ∅ → (𝑊 Σg
(𝑘 ∈ 𝑎 ↦ 𝑄)) = (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄))) |
9 | 8 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = ∅ → (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄)))) |
10 | 6, 9 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑎 = ∅ → ((𝑊 Σg
(𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) ↔ (𝑊 Σg (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄))))) |
11 | 4, 10 | imbi12d 333 |
. . . . 5
⊢ (𝑎 = ∅ → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄)))))) |
12 | | sseq1 3589 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → (𝑎 ⊆ 𝐴 ↔ 𝑒 ⊆ 𝐴)) |
13 | 12 | anbi2d 736 |
. . . . . 6
⊢ (𝑎 = 𝑒 → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑒 ⊆ 𝐴))) |
14 | | mpteq1 4665 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄)) = (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) |
15 | 14 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄)))) |
16 | | mpteq1 4665 |
. . . . . . . . 9
⊢ (𝑎 = 𝑒 → (𝑘 ∈ 𝑎 ↦ 𝑄) = (𝑘 ∈ 𝑒 ↦ 𝑄)) |
17 | 16 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = 𝑒 → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)) = (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) |
18 | 17 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = 𝑒 → (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) |
19 | 15, 18 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑎 = 𝑒 → ((𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) ↔ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))))) |
20 | 13, 19 | imbi12d 333 |
. . . . 5
⊢ (𝑎 = 𝑒 → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)))) ↔ ((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))))) |
21 | | sseq1 3589 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (𝑎 ⊆ 𝐴 ↔ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) |
22 | 21 | anbi2d 736 |
. . . . . 6
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴))) |
23 | | mpteq1 4665 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄)) = (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) |
24 | 23 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄)))) |
25 | | mpteq1 4665 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (𝑘 ∈ 𝑎 ↦ 𝑄) = (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)) |
26 | 25 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)) = (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄))) |
27 | 26 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)))) |
28 | 24, 27 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → ((𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) ↔ (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄))))) |
29 | 22, 28 | imbi12d 333 |
. . . . 5
⊢ (𝑎 = (𝑒 ∪ {𝑧}) → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)))) ↔ ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)))))) |
30 | | sseq1 3589 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
31 | 30 | anbi2d 736 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝜑 ∧ 𝑎 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴))) |
32 | | mpteq1 4665 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄)) = (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) |
33 | 32 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄)))) |
34 | | mpteq1 4665 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑘 ∈ 𝑎 ↦ 𝑄) = (𝑘 ∈ 𝐴 ↦ 𝑄)) |
35 | 34 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)) = (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄))) |
36 | 35 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))) |
37 | 33, 36 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄))) ↔ (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄))))) |
38 | 31, 37 | imbi12d 333 |
. . . . 5
⊢ (𝑎 = 𝐴 → (((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑎 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑎 ↦ 𝑄)))) ↔ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))))) |
39 | | gsumvsca.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ SLMod) |
40 | | gsumvsca.k |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ⊆ (Base‘𝐺)) |
41 | | gsumvsca1.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ 𝐾) |
42 | 40, 41 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (Base‘𝐺)) |
43 | | gsumvsca.g |
. . . . . . . . . 10
⊢ 𝐺 = (Scalar‘𝑊) |
44 | | gsumvsca.t |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
45 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝐺) =
(Base‘𝐺) |
46 | | gsumvsca.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑊) |
47 | 43, 44, 45, 46 | slmdvs0 29109 |
. . . . . . . . 9
⊢ ((𝑊 ∈ SLMod ∧ 𝑃 ∈ (Base‘𝐺)) → (𝑃 · 0 ) = 0 ) |
48 | 39, 42, 47 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 · 0 ) = 0 ) |
49 | 48 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → 0 = (𝑃 · 0 )) |
50 | | mpt0 5934 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄)) = ∅ |
51 | 50 | oveq2i 6560 |
. . . . . . . 8
⊢ (𝑊 Σg
(𝑘 ∈ ∅ ↦
(𝑃 · 𝑄))) = (𝑊 Σg
∅) |
52 | 46 | gsum0 17101 |
. . . . . . . 8
⊢ (𝑊 Σg
∅) = 0 |
53 | 51, 52 | eqtri 2632 |
. . . . . . 7
⊢ (𝑊 Σg
(𝑘 ∈ ∅ ↦
(𝑃 · 𝑄))) = 0 |
54 | | mpt0 5934 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∅ ↦ 𝑄) = ∅ |
55 | 54 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝑊 Σg
(𝑘 ∈ ∅ ↦
𝑄)) = (𝑊 Σg
∅) |
56 | 55, 52 | eqtri 2632 |
. . . . . . . 8
⊢ (𝑊 Σg
(𝑘 ∈ ∅ ↦
𝑄)) = 0 |
57 | 56 | oveq2i 6560 |
. . . . . . 7
⊢ (𝑃 · (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄))) = (𝑃 · 0 ) |
58 | 49, 53, 57 | 3eqtr4g 2669 |
. . . . . 6
⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄)))) |
59 | 58 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ ∅ ↦ 𝑄)))) |
60 | | ssun1 3738 |
. . . . . . . . 9
⊢ 𝑒 ⊆ (𝑒 ∪ {𝑧}) |
61 | | sstr2 3575 |
. . . . . . . . 9
⊢ (𝑒 ⊆ (𝑒 ∪ {𝑧}) → ((𝑒 ∪ {𝑧}) ⊆ 𝐴 → 𝑒 ⊆ 𝐴)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑒 ∪ {𝑧}) ⊆ 𝐴 → 𝑒 ⊆ 𝐴) |
63 | 62 | anim2i 591 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝜑 ∧ 𝑒 ⊆ 𝐴)) |
64 | 63 | imim1i 61 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))))) |
65 | 39 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑊 ∈ SLMod) |
66 | 42 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑃 ∈ (Base‘𝐺)) |
67 | | gsumvsca.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑊) |
68 | | slmdcmn 29089 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ SLMod → 𝑊 ∈ CMnd) |
69 | 65, 68 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑊 ∈ CMnd) |
70 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑒 ∈ V |
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑒 ∈ V) |
72 | | simplrl 796 |
. . . . . . . . . . . . . 14
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝜑) |
73 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑒 ∪ {𝑧}) ⊆ 𝐴) |
74 | 73 | unssad 3752 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑒 ⊆ 𝐴) |
75 | 74 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑘 ∈ 𝐴) |
76 | | gsumvsca1.c |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑄 ∈ 𝐵) |
77 | 72, 75, 76 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑄 ∈ 𝐵) |
78 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑒 ↦ 𝑄) = (𝑘 ∈ 𝑒 ↦ 𝑄) |
79 | 77, 78 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑘 ∈ 𝑒 ↦ 𝑄):𝑒⟶𝐵) |
80 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑒 ∈ Fin) |
81 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑊) ∈ V |
82 | 46, 81 | eqeltri 2684 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
83 | 82 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 0 ∈ V) |
84 | 78, 80, 77, 83 | fsuppmptdm 8169 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑘 ∈ 𝑒 ↦ 𝑄) finSupp 0 ) |
85 | 67, 46, 69, 71, 79, 84 | gsumcl 18139 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) ∈ 𝐵) |
86 | 73 | unssbd 3753 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴) |
87 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
88 | 87 | snss 4259 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
89 | 86, 88 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴) |
90 | 76 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑄 ∈ 𝐵) |
91 | 90 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ∀𝑘 ∈ 𝐴 𝑄 ∈ 𝐵) |
92 | | rspcsbela 3958 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝑄 ∈ 𝐵) → ⦋𝑧 / 𝑘⦌𝑄 ∈ 𝐵) |
93 | 89, 91, 92 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ⦋𝑧 / 𝑘⦌𝑄 ∈ 𝐵) |
94 | | gsumvsca.p |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝑊) |
95 | 67, 94, 43, 44, 45 | slmdvsdi 29099 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ SLMod ∧ (𝑃 ∈ (Base‘𝐺) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝑄 ∈ 𝐵)) → (𝑃 · ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) + ⦋𝑧 / 𝑘⦌𝑄)) = ((𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
96 | 65, 66, 85, 93, 95 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑃 · ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) + ⦋𝑧 / 𝑘⦌𝑄)) = ((𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
97 | 96 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → (𝑃 · ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) + ⦋𝑧 / 𝑘⦌𝑄)) = ((𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
98 | | nfcsb1v 3515 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝑄 |
99 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V) |
100 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑒) |
101 | | csbeq1a 3508 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → 𝑄 = ⦋𝑧 / 𝑘⦌𝑄) |
102 | 98, 67, 94, 69, 80, 77, 99, 100, 93, 101 | gsumunsnf 18181 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)) = ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) + ⦋𝑧 / 𝑘⦌𝑄)) |
103 | 102 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄))) = (𝑃 · ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) + ⦋𝑧 / 𝑘⦌𝑄))) |
104 | 103 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄))) = (𝑃 · ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)) + ⦋𝑧 / 𝑘⦌𝑄))) |
105 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘𝑃 |
106 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘
· |
107 | 105, 106,
98 | nfov 6575 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝑃 ·
⦋𝑧 / 𝑘⦌𝑄) |
108 | 72, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑊 ∈ SLMod) |
109 | 72, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑃 ∈ (Base‘𝐺)) |
110 | 67, 43, 44, 45 | slmdvscl 29098 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ SLMod ∧ 𝑃 ∈ (Base‘𝐺) ∧ 𝑄 ∈ 𝐵) → (𝑃 · 𝑄) ∈ 𝐵) |
111 | 108, 109,
77, 110 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → (𝑃 · 𝑄) ∈ 𝐵) |
112 | 67, 43, 44, 45 | slmdvscl 29098 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ SLMod ∧ 𝑃 ∈ (Base‘𝐺) ∧ ⦋𝑧 / 𝑘⦌𝑄 ∈ 𝐵) → (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄) ∈ 𝐵) |
113 | 65, 66, 93, 112 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄) ∈ 𝐵) |
114 | 101 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → (𝑃 · 𝑄) = (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄)) |
115 | 107, 67, 94, 69, 80, 111, 99, 100, 113, 114 | gsumunsnf 18181 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
116 | 115 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
117 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) |
118 | 117 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄)) = ((𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
119 | 116, 118 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) + (𝑃 ·
⦋𝑧 / 𝑘⦌𝑄))) |
120 | 97, 104, 119 | 3eqtr4rd 2655 |
. . . . . . . 8
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)))) |
121 | 120 | exp31 628 |
. . . . . . 7
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄))) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)))))) |
122 | 121 | a2d 29 |
. . . . . 6
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) → (((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)))))) |
123 | 64, 122 | syl5 33 |
. . . . 5
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) → (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝑒 ↦ 𝑄)))) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑄)))))) |
124 | 11, 20, 29, 38, 59, 123 | findcard2s 8086 |
. . . 4
⊢ (𝐴 ∈ Fin → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄))))) |
125 | 124 | imp 444 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝜑 ∧ 𝐴 ⊆ 𝐴)) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))) |
126 | 2, 125 | mpanr2 716 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝜑) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))) |
127 | 1, 126 | mpancom 700 |
1
⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = (𝑃 · (𝑊 Σg (𝑘 ∈ 𝐴 ↦ 𝑄)))) |