Step | Hyp | Ref
| Expression |
1 | | simp1 1138 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → 𝑀 ∈ LMod) |
2 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
3 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘𝑀) =
(LSubSp‘𝑀) |
4 | 2, 3 | lssss 19978 |
. . . . . 6
⊢ (𝑆 ∈ (LSubSp‘𝑀) → 𝑆 ⊆ (Base‘𝑀)) |
5 | 4 | 3ad2ant2 1136 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → 𝑆 ⊆ (Base‘𝑀)) |
6 | | sstr 3914 |
. . . . . . . 8
⊢ ((𝑉 ⊆ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑀)) → 𝑉 ⊆ (Base‘𝑀)) |
7 | | fvex 6735 |
. . . . . . . . . 10
⊢
(Base‘𝑀)
∈ V |
8 | 7 | ssex 5219 |
. . . . . . . . 9
⊢ (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ V) |
9 | | elpwg 4521 |
. . . . . . . . . 10
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫
(Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
10 | 9 | biimprd 251 |
. . . . . . . . 9
⊢ (𝑉 ∈ V → (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀))) |
11 | 8, 10 | mpcom 38 |
. . . . . . . 8
⊢ (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
12 | 6, 11 | syl 17 |
. . . . . . 7
⊢ ((𝑉 ⊆ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑀)) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
13 | 12 | ex 416 |
. . . . . 6
⊢ (𝑉 ⊆ 𝑆 → (𝑆 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀))) |
14 | 13 | 3ad2ant3 1137 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → (𝑆 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀))) |
15 | 5, 14 | mpd 15 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
16 | | eqid 2737 |
. . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
17 | | eqid 2737 |
. . . . 5
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
18 | 2, 16, 17 | lcoval 45434 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑥 ∈ (𝑀 LinCo 𝑉) ↔ (𝑥 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉))))) |
19 | 1, 15, 18 | syl2anc 587 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → (𝑥 ∈ (𝑀 LinCo 𝑉) ↔ (𝑥 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉))))) |
20 | | lincellss 45448 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀))) → (𝑓( linC ‘𝑀)𝑉) ∈ 𝑆)) |
21 | 20 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ (𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀)))) → (𝑓( linC ‘𝑀)𝑉) ∈ 𝑆) |
22 | | eleq1 2825 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑓( linC ‘𝑀)𝑉) → (𝑥 ∈ 𝑆 ↔ (𝑓( linC ‘𝑀)𝑉) ∈ 𝑆)) |
23 | 21, 22 | syl5ibr 249 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓( linC ‘𝑀)𝑉) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ (𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀)))) → 𝑥 ∈ 𝑆)) |
24 | 23 | expd 419 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓( linC ‘𝑀)𝑉) → ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀))) → 𝑥 ∈ 𝑆))) |
25 | 24 | com12 32 |
. . . . . . . . 9
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → (𝑥 = (𝑓( linC ‘𝑀)𝑉) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀))) → 𝑥 ∈ 𝑆))) |
26 | 25 | adantr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝑥 = (𝑓( linC ‘𝑀)𝑉) → ((𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀))) → 𝑥 ∈ 𝑆))) |
27 | 26 | com13 88 |
. . . . . . 7
⊢ ((𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑓 finSupp
(0g‘(Scalar‘𝑀))) → (𝑥 = (𝑓( linC ‘𝑀)𝑉) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥 ∈ 𝑆))) |
28 | 27 | impr 458 |
. . . . . 6
⊢ ((𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ (𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉))) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥 ∈ 𝑆)) |
29 | 28 | rexlimiva 3205 |
. . . . 5
⊢
(∃𝑓 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉)) → (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → 𝑥 ∈ 𝑆)) |
30 | 29 | com12 32 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) ∧ 𝑥 ∈ (Base‘𝑀)) → (∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉)) → 𝑥 ∈ 𝑆)) |
31 | 30 | expimpd 457 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ((𝑥 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑥 = (𝑓( linC ‘𝑀)𝑉))) → 𝑥 ∈ 𝑆)) |
32 | 19, 31 | sylbid 243 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → (𝑥 ∈ (𝑀 LinCo 𝑉) → 𝑥 ∈ 𝑆)) |
33 | 32 | ralrimiv 3104 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑀) ∧ 𝑉 ⊆ 𝑆) → ∀𝑥 ∈ (𝑀 LinCo 𝑉)𝑥 ∈ 𝑆) |