Step | Hyp | Ref
| Expression |
1 | | elelpwi 4500 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑣 ∈ (Base‘𝑀)) |
2 | 1 | expcom 417 |
. . . . . 6
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑣 ∈ 𝑉 → 𝑣 ∈ (Base‘𝑀))) |
3 | 2 | adantl 485 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑣 ∈ 𝑉 → 𝑣 ∈ (Base‘𝑀))) |
4 | 3 | imp 410 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Base‘𝑀)) |
5 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
6 | | eqid 2738 |
. . . . . . 7
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
7 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑀)) =
(0g‘(Scalar‘𝑀)) |
8 | | eqid 2738 |
. . . . . . 7
⊢
(1r‘(Scalar‘𝑀)) =
(1r‘(Scalar‘𝑀)) |
9 | | equequ1 2037 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑣 ↔ 𝑦 = 𝑣)) |
10 | 9 | ifbid 4437 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) = if(𝑦 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) |
11 | 10 | cbvmptv 5133 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) = (𝑦 ∈ 𝑉 ↦ if(𝑦 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) |
12 | 5, 6, 7, 8, 11 | mptcfsupp 45250 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝑣 ∈ 𝑉) → (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀))) |
13 | 12 | 3expa 1119 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀))) |
14 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) |
15 | 5, 6, 7, 8, 14 | linc1 45300 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝑣 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉) = 𝑣) |
16 | 15 | 3expa 1119 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉) = 𝑣) |
17 | 16 | eqcomd 2744 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → 𝑣 = ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉)) |
18 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
19 | 6, 18, 8 | lmod1cl 19780 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(1r‘(Scalar‘𝑀)) ∈ (Base‘(Scalar‘𝑀))) |
20 | 6, 18, 7 | lmod0cl 19779 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(0g‘(Scalar‘𝑀)) ∈ (Base‘(Scalar‘𝑀))) |
21 | 19, 20 | ifcld 4460 |
. . . . . . . . 9
⊢ (𝑀 ∈ LMod → if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) ∈ (Base‘(Scalar‘𝑀))) |
22 | 21 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))) ∈ (Base‘(Scalar‘𝑀))) |
23 | 22 | fmpttd 6889 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑉⟶(Base‘(Scalar‘𝑀))) |
24 | | fvex 6687 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
25 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
26 | | elmapg 8450 |
. . . . . . . 8
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
27 | 24, 25, 26 | sylancr 590 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
28 | 23, 27 | mpbird 260 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
29 | | breq1 5033 |
. . . . . . . 8
⊢ (𝑓 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓 finSupp
(0g‘(Scalar‘𝑀)) ↔ (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)))) |
30 | | oveq1 7177 |
. . . . . . . . 9
⊢ (𝑓 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑓( linC ‘𝑀)𝑉) = ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉)) |
31 | 30 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑓 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → (𝑣 = (𝑓( linC ‘𝑀)𝑉) ↔ 𝑣 = ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉))) |
32 | 29, 31 | anbi12d 634 |
. . . . . . 7
⊢ (𝑓 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) → ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑓( linC ‘𝑀)𝑉)) ↔ ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉)))) |
33 | 32 | adantl 485 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑓 = (𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))) → ((𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑓( linC ‘𝑀)𝑉)) ↔ ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉)))) |
34 | 28, 33 | rspcedv 3519 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → (((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀)))) finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = ((𝑥 ∈ 𝑉 ↦ if(𝑥 = 𝑣, (1r‘(Scalar‘𝑀)),
(0g‘(Scalar‘𝑀))))( linC ‘𝑀)𝑉)) → ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑓( linC ‘𝑀)𝑉)))) |
35 | 13, 17, 34 | mp2and 699 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑓( linC ‘𝑀)𝑉))) |
36 | 5, 6, 18 | lcoval 45287 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑣 ∈ (𝑀 LinCo 𝑉) ↔ (𝑣 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑓( linC ‘𝑀)𝑉))))) |
37 | 36 | adantr 484 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → (𝑣 ∈ (𝑀 LinCo 𝑉) ↔ (𝑣 ∈ (Base‘𝑀) ∧ ∃𝑓 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)(𝑓 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑓( linC ‘𝑀)𝑉))))) |
38 | 4, 35, 37 | mpbir2and 713 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (𝑀 LinCo 𝑉)) |
39 | 38 | ex 416 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑣 ∈ 𝑉 → 𝑣 ∈ (𝑀 LinCo 𝑉))) |
40 | 39 | ssrdv 3883 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ⊆ (𝑀 LinCo 𝑉)) |