| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
| 4 | 1, 2, 3 | lcoval 48329 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝐶 ∈ (𝑀 LinCo 𝑉) ↔ (𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))))) |
| 5 | 1, 2, 3 | lcoval 48329 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝐷 ∈ (𝑀 LinCo 𝑉) ↔ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) |
| 6 | 4, 5 | anbi12d 632 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) ↔ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))))) |
| 7 | | simpll 767 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝑀 ∈ LMod) |
| 8 | | simpll 767 |
. . . . . . 7
⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐶 ∈ (Base‘𝑀)) |
| 9 | 8 | adantl 481 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝐶 ∈ (Base‘𝑀)) |
| 10 | | simprl 771 |
. . . . . . 7
⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐷 ∈ (Base‘𝑀)) |
| 11 | 10 | adantl 481 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝐷 ∈ (Base‘𝑀)) |
| 12 | | lincsumcl.b |
. . . . . . 7
⊢ + =
(+g‘𝑀) |
| 13 | 1, 12 | lmodvacl 20873 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → (𝐶 + 𝐷) ∈ (Base‘𝑀)) |
| 14 | 7, 9, 11, 13 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → (𝐶 + 𝐷) ∈ (Base‘𝑀)) |
| 15 | 2 | lmodfgrp 20867 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Grp) |
| 16 | 15 | grpmndd 18964 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Mnd) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(Scalar‘𝑀) ∈
Mnd) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (Scalar‘𝑀) ∈ Mnd) |
| 19 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
| 21 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → 𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 22 | | simpl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 23 | 21, 22 | anim12i 613 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(Scalar‘𝑀)) =
(+g‘(Scalar‘𝑀)) |
| 26 | 3, 25 | ofaddmndmap 48259 |
. . . . . . . . . . . . . . . 16
⊢
(((Scalar‘𝑀)
∈ Mnd ∧ 𝑉 ∈
𝒫 (Base‘𝑀)
∧ (𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))) → (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 27 | 18, 20, 24, 26 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 28 | 16 | anim1i 615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((Scalar‘𝑀) ∈
Mnd ∧ 𝑉 ∈
𝒫 (Base‘𝑀))) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ((Scalar‘𝑀) ∈ Mnd ∧ 𝑉 ∈ 𝒫
(Base‘𝑀))) |
| 30 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → 𝑦 finSupp
(0g‘(Scalar‘𝑀))) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → 𝑦 finSupp
(0g‘(Scalar‘𝑀))) |
| 32 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 finSupp
(0g‘(Scalar‘𝑀))) |
| 33 | 31, 32 | anim12i 613 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) |
| 35 | 3 | mndpfsupp 18780 |
. . . . . . . . . . . . . . . 16
⊢
((((Scalar‘𝑀)
∈ Mnd ∧ 𝑉 ∈
𝒫 (Base‘𝑀))
∧ (𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) → (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀))) |
| 36 | 29, 24, 34, 35 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀))) |
| 37 | | oveq12 7440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶 = (𝑦( linC ‘𝑀)𝑉) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))) |
| 38 | 37 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐷 = (𝑥( linC ‘𝑀)𝑉) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐶 = (𝑦( linC ‘𝑀)𝑉) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))) |
| 45 | 44 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))) |
| 47 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦( linC ‘𝑀)𝑉) = (𝑦( linC ‘𝑀)𝑉) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥( linC ‘𝑀)𝑉) = (𝑥( linC ‘𝑀)𝑉) |
| 50 | 12, 48, 49, 2, 3, 25 | lincsum 48346 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀)))) → ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
| 51 | 47, 24, 34, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
| 52 | 46, 51 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝐶 + 𝐷) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
| 53 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) → (𝑠 finSupp
(0g‘(Scalar‘𝑀)) ↔ (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀)))) |
| 54 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) → (𝑠( linC ‘𝑀)𝑉) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)) |
| 55 | 54 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) → ((𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉) ↔ (𝐶 + 𝐷) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))) |
| 56 | 53, 55 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) → ((𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)) ↔ ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)))) |
| 57 | 56 | rspcev 3622 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥) finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = ((𝑦 ∘f
(+g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
| 58 | 27, 36, 52, 57 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢
(((((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
| 59 | 58 | exp41 434 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
| 60 | 59 | rexlimiva 3147 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → ((𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
| 61 | 60 | expd 415 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → (𝐶 ∈ (Base‘𝑀) → (𝐷 ∈ (Base‘𝑀) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))) |
| 62 | 61 | impcom 407 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
| 63 | 62 | com13 88 |
. . . . . . . . 9
⊢ ((𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
| 64 | 63 | rexlimiva 3147 |
. . . . . . . 8
⊢
(∃𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐷 ∈ (Base‘𝑀) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))) |
| 65 | 64 | impcom 407 |
. . . . . . 7
⊢ ((𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
| 66 | 65 | impcom 407 |
. . . . . 6
⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))) |
| 67 | 66 | impcom 407 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
| 68 | 1, 2, 3 | lcoval 48329 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 + 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
| 69 | 68 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → ((𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 + 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
| 70 | 14, 67, 69 | mpbir2and 713 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)) |
| 71 | 70 | ex 412 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(((𝐶 ∈
(Base‘𝑀) ∧
∃𝑦 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑦 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))) |
| 72 | 6, 71 | sylbid 240 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))) |
| 73 | 72 | imp 406 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)) |