Step | Hyp | Ref
| Expression |
1 | | eqid 2825 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2825 |
. . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
3 | | eqid 2825 |
. . . . 5
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
4 | 1, 2, 3 | lcoval 43066 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝐶 ∈ (𝑀 LinCo 𝑉) ↔ (𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))))) |
5 | 1, 2, 3 | lcoval 43066 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝐷 ∈ (𝑀 LinCo 𝑉) ↔ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) |
6 | 4, 5 | anbi12d 624 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) ↔ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))))) |
7 | | simpll 783 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝑀 ∈ LMod) |
8 | | simpll 783 |
. . . . . . 7
⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐶 ∈ (Base‘𝑀)) |
9 | 8 | adantl 475 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝐶 ∈ (Base‘𝑀)) |
10 | | simprl 787 |
. . . . . . 7
⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐷 ∈ (Base‘𝑀)) |
11 | 10 | adantl 475 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝐷 ∈ (Base‘𝑀)) |
12 | | lincsumcl.b |
. . . . . . 7
⊢ + =
(+g‘𝑀) |
13 | 1, 12 | lmodvacl 19240 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → (𝐶 + 𝐷) ∈ (Base‘𝑀)) |
14 | 7, 9, 11, 13 | syl3anc 1494 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → (𝐶 + 𝐷) ∈ (Base‘𝑀)) |
15 | 2 | lmodfgrp 19235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Grp) |
16 | | grpmnd 17790 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Scalar‘𝑀)
∈ Grp → (Scalar‘𝑀) ∈ Mnd) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Mnd) |
18 | 17 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(Scalar‘𝑀) ∈
Mnd) |
19 | 18 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (Scalar‘𝑀) ∈ Mnd) |
20 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
21 | 20 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
22 | | simpll 783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → 𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
23 | | simpl 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
24 | 22, 23 | anim12i 606 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉))) |
25 | 24 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉))) |
26 | | eqid 2825 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(Scalar‘𝑀)) =
(+g‘(Scalar‘𝑀)) |
27 | 3, 26 | ofaddmndmap 42987 |
. . . . . . . . . . . . . . . 16
⊢
(((Scalar‘𝑀)
∈ Mnd ∧ 𝑉 ∈
𝒫 (Base‘𝑀)
∧ (𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉))) → (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
28 | 19, 21, 25, 27 | syl3anc 1494 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
29 | 17 | anim1i 608 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((Scalar‘𝑀) ∈
Mnd ∧ 𝑉 ∈
𝒫 (Base‘𝑀))) |
30 | 29 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ((Scalar‘𝑀) ∈ Mnd ∧ 𝑉 ∈ 𝒫
(Base‘𝑀))) |
31 | | simprl 787 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → 𝑦 finSupp
(0g‘(Scalar‘𝑀))) |
32 | 31 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → 𝑦 finSupp
(0g‘(Scalar‘𝑀))) |
33 | | simprl 787 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 finSupp
(0g‘(Scalar‘𝑀))) |
34 | 32, 33 | anim12i 606 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) |
35 | 34 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) |
36 | 3 | mndpfsupp 43022 |
. . . . . . . . . . . . . . . 16
⊢
((((Scalar‘𝑀)
∈ Mnd ∧ 𝑉 ∈
𝒫 (Base‘𝑀))
∧ (𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) → (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀))) |
37 | 30, 25, 35, 36 | syl3anc 1494 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀))) |
38 | | oveq12 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶 = (𝑦( linC ‘𝑀)𝑉) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))) |
39 | 38 | expcom 404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐷 = (𝑥( linC ‘𝑀)𝑉) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
40 | 39 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
41 | 40 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
42 | 41 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 = (𝑦( linC ‘𝑀)𝑉) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
43 | 42 | adantl 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
44 | 43 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
45 | 44 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
46 | 45 | imp 397 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))) |
47 | 46 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))) |
48 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
49 | | eqid 2825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦( linC ‘𝑀)𝑉) = (𝑦( linC ‘𝑀)𝑉) |
50 | | eqid 2825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥( linC ‘𝑀)𝑉) = (𝑥( linC ‘𝑀)𝑉) |
51 | 12, 49, 50, 2, 3, 26 | lincsum 43083 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) → ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
52 | 48, 25, 35, 51 | syl3anc 1494 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
53 | 47, 52 | eqtrd 2861 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝐶 + 𝐷) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
54 | | breq1 4878 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) → (𝑠 finSupp
(0g‘(Scalar‘𝑀)) ↔ (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀)))) |
55 | | oveq1 6917 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) → (𝑠( linC ‘𝑀)𝑉) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
56 | 55 | eqeq2d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) → ((𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉) ↔ (𝐶 + 𝐷) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))) |
57 | 54, 56 | anbi12d 624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) → ((𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)) ↔ ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)))) |
58 | 57 | rspcev 3526 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = ((𝑦 ∘𝑓
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
59 | 28, 37, 53, 58 | syl12anc 870 |
. . . . . . . . . . . . . 14
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
60 | 59 | exp41 427 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
61 | 60 | rexlimiva 3237 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → ((𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
62 | 61 | expd 406 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → (𝐶 ∈ (Base‘𝑀) → (𝐷 ∈ (Base‘𝑀) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))) |
63 | 62 | impcom 398 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
64 | 63 | com13 88 |
. . . . . . . . 9
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
65 | 64 | rexlimiva 3237 |
. . . . . . . 8
⊢
(∃𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐷 ∈ (Base‘𝑀) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
66 | 65 | impcom 398 |
. . . . . . 7
⊢ ((𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
67 | 66 | impcom 398 |
. . . . . 6
⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))) |
68 | 67 | impcom 398 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
69 | 1, 2, 3 | lcoval 43066 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 + 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
70 | 69 | adantr 474 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → ((𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 + 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
71 | 14, 68, 70 | mpbir2and 704 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)) |
72 | 71 | ex 403 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))) |
73 | 6, 72 | sylbid 232 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))) |
74 | 73 | imp 397 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)) |