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 | oveq1d 6564 |
. . . . . . 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 | oveq1d 6564 |
. . . . . . 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 | oveq1d 6564 |
. . . . . . 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 | oveq1d 6564 |
. . . . . . 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 | | gsumvsca2.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ 𝐵) |
41 | | gsumvsca.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑊) |
42 | | gsumvsca.g |
. . . . . . . . . 10
⊢ 𝐺 = (Scalar‘𝑊) |
43 | | gsumvsca.t |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
44 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
45 | | gsumvsca.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑊) |
46 | 41, 42, 43, 44, 45 | slmd0vs 29108 |
. . . . . . . . 9
⊢ ((𝑊 ∈ SLMod ∧ 𝑄 ∈ 𝐵) → ((0g‘𝐺) · 𝑄) = 0 ) |
47 | 39, 40, 46 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 →
((0g‘𝐺)
·
𝑄) = 0 ) |
48 | 47 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → 0 =
((0g‘𝐺)
·
𝑄)) |
49 | | mpt0 5934 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∅ ↦ (𝑃 · 𝑄)) = ∅ |
50 | 49 | oveq2i 6560 |
. . . . . . . 8
⊢ (𝑊 Σg
(𝑘 ∈ ∅ ↦
(𝑃 · 𝑄))) = (𝑊 Σg
∅) |
51 | 45 | gsum0 17101 |
. . . . . . . 8
⊢ (𝑊 Σg
∅) = 0 |
52 | 50, 51 | eqtri 2632 |
. . . . . . 7
⊢ (𝑊 Σg
(𝑘 ∈ ∅ ↦
(𝑃 · 𝑄))) = 0 |
53 | | mpt0 5934 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∅ ↦ 𝑃) = ∅ |
54 | 53 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝐺 Σg
(𝑘 ∈ ∅ ↦
𝑃)) = (𝐺 Σg
∅) |
55 | 44 | gsum0 17101 |
. . . . . . . . 9
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
56 | 54, 55 | eqtri 2632 |
. . . . . . . 8
⊢ (𝐺 Σg
(𝑘 ∈ ∅ ↦
𝑃)) =
(0g‘𝐺) |
57 | 56 | oveq1i 6559 |
. . . . . . 7
⊢ ((𝐺 Σg
(𝑘 ∈ ∅ ↦
𝑃)) · 𝑄) = ((0g‘𝐺) · 𝑄) |
58 | 48, 52, 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 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺) =
(Base‘𝐺) |
67 | 42 | slmdsrg 29091 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ SLMod → 𝐺 ∈ SRing) |
68 | | srgcmn 18331 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ SRing → 𝐺 ∈ CMnd) |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . 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 | | gsumvsca.k |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ⊆ (Base‘𝐺)) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐾 ⊆ (Base‘𝐺)) |
78 | | gsumvsca2.c |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐾) |
79 | 77, 78 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ (Base‘𝐺)) |
80 | 72, 75, 79 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑃 ∈ (Base‘𝐺)) |
81 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑒 ↦ 𝑃) = (𝑘 ∈ 𝑒 ↦ 𝑃) |
82 | 80, 81 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑘 ∈ 𝑒 ↦ 𝑃):𝑒⟶(Base‘𝐺)) |
83 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑒 ∈ Fin) |
84 | 72, 75, 78 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑃 ∈ 𝐾) |
85 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) ∈ V |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (0g‘𝐺) ∈ V) |
87 | 81, 83, 84, 86 | fsuppmptdm 8169 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑘 ∈ 𝑒 ↦ 𝑃) finSupp (0g‘𝐺)) |
88 | 66, 44, 69, 71, 82, 87 | gsumcl 18139 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) ∈ (Base‘𝐺)) |
89 | 73 | unssbd 3753 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴) |
90 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
91 | 90 | snss 4259 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
92 | 89, 91 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴) |
93 | 79 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑃 ∈ (Base‘𝐺)) |
94 | 93 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ∀𝑘 ∈ 𝐴 𝑃 ∈ (Base‘𝐺)) |
95 | | rspcsbela 3958 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝑃 ∈ (Base‘𝐺)) → ⦋𝑧 / 𝑘⦌𝑃 ∈ (Base‘𝐺)) |
96 | 92, 94, 95 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ⦋𝑧 / 𝑘⦌𝑃 ∈ (Base‘𝐺)) |
97 | 40 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑄 ∈ 𝐵) |
98 | | gsumvsca.p |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝑊) |
99 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
100 | 41, 98, 42, 43, 66, 99 | slmdvsdir 29100 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ SLMod ∧ ((𝐺 Σg
(𝑘 ∈ 𝑒 ↦ 𝑃)) ∈ (Base‘𝐺) ∧ ⦋𝑧 / 𝑘⦌𝑃 ∈ (Base‘𝐺) ∧ 𝑄 ∈ 𝐵)) → (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃))(+g‘𝐺)⦋𝑧 / 𝑘⦌𝑃) · 𝑄) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
101 | 65, 88, 96, 97, 100 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃))(+g‘𝐺)⦋𝑧 / 𝑘⦌𝑃) · 𝑄) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
102 | 101 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃))(+g‘𝐺)⦋𝑧 / 𝑘⦌𝑃) · 𝑄) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
103 | | nfcsb1v 3515 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝑃 |
104 | 90 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V) |
105 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑒) |
106 | | csbeq1a 3508 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → 𝑃 = ⦋𝑧 / 𝑘⦌𝑃) |
107 | 103, 66, 99, 69, 83, 80, 104, 105, 96, 106 | gsumunsnf 18181 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃))(+g‘𝐺)⦋𝑧 / 𝑘⦌𝑃)) |
108 | 107 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → ((𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) · 𝑄) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃))(+g‘𝐺)⦋𝑧 / 𝑘⦌𝑃) · 𝑄)) |
109 | 108 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → ((𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) · 𝑄) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃))(+g‘𝐺)⦋𝑧 / 𝑘⦌𝑃) · 𝑄)) |
110 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘
· |
111 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘𝑄 |
112 | 103, 110,
111 | nfov 6575 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(⦋𝑧 / 𝑘⦌𝑃 · 𝑄) |
113 | | slmdcmn 29089 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ SLMod → 𝑊 ∈ CMnd) |
114 | 65, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → 𝑊 ∈ CMnd) |
115 | 72, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑊 ∈ SLMod) |
116 | 72, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → 𝑄 ∈ 𝐵) |
117 | 41, 42, 43, 66 | slmdvscl 29098 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ SLMod ∧ 𝑃 ∈ (Base‘𝐺) ∧ 𝑄 ∈ 𝐵) → (𝑃 · 𝑄) ∈ 𝐵) |
118 | 115, 80, 116, 117 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ 𝑘 ∈ 𝑒) → (𝑃 · 𝑄) ∈ 𝐵) |
119 | 41, 42, 43, 66 | slmdvscl 29098 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ SLMod ∧
⦋𝑧 / 𝑘⦌𝑃 ∈ (Base‘𝐺) ∧ 𝑄 ∈ 𝐵) → (⦋𝑧 / 𝑘⦌𝑃 · 𝑄) ∈ 𝐵) |
120 | 65, 96, 97, 119 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (⦋𝑧 / 𝑘⦌𝑃 · 𝑄) ∈ 𝐵) |
121 | 106 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → (𝑃 · 𝑄) = (⦋𝑧 / 𝑘⦌𝑃 · 𝑄)) |
122 | 112, 41, 98, 114, 83, 118, 104, 105, 120, 121 | gsumunsnf 18181 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
123 | 122 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
124 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) |
125 | 124 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄)) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
126 | 123, 125 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = (((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄) + (⦋𝑧 / 𝑘⦌𝑃 · 𝑄))) |
127 | 102, 109,
126 | 3eqtr4rd 2655 |
. . . . . . . 8
⊢ ((((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴)) ∧ (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) · 𝑄)) |
128 | 127 | exp31 628 |
. . . . . . 7
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → ((𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) · 𝑄)))) |
129 | 128 | a2d 29 |
. . . . . 6
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) → (((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) · 𝑄)))) |
130 | 64, 129 | syl5 33 |
. . . . 5
⊢ ((𝑒 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑒) → (((𝜑 ∧ 𝑒 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝑒 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝑒 ↦ 𝑃)) · 𝑄)) → ((𝜑 ∧ (𝑒 ∪ {𝑧}) ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ (𝑒 ∪ {𝑧}) ↦ 𝑃)) · 𝑄)))) |
131 | 11, 20, 29, 38, 59, 130 | findcard2s 8086 |
. . . 4
⊢ (𝐴 ∈ Fin → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑃)) · 𝑄))) |
132 | 131 | imp 444 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ (𝜑 ∧ 𝐴 ⊆ 𝐴)) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑃)) · 𝑄)) |
133 | 2, 132 | mpanr2 716 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝜑) → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑃)) · 𝑄)) |
134 | 1, 133 | mpancom 700 |
1
⊢ (𝜑 → (𝑊 Σg (𝑘 ∈ 𝐴 ↦ (𝑃 · 𝑄))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑃)) · 𝑄)) |