Proof of Theorem lmodvscl
Step | Hyp | Ref
| Expression |
1 | | biid 264 |
. 2
⊢ (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod) |
2 | | pm4.24 567 |
. 2
⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) |
3 | | pm4.24 567 |
. 2
⊢ (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) |
4 | | lmodvscl.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
5 | | eqid 2739 |
. . . . 5
⊢
(+g‘𝑊) = (+g‘𝑊) |
6 | | lmodvscl.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
7 | | lmodvscl.f |
. . . . 5
⊢ 𝐹 = (Scalar‘𝑊) |
8 | | lmodvscl.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐹) |
9 | | eqid 2739 |
. . . . 5
⊢
(+g‘𝐹) = (+g‘𝐹) |
10 | | eqid 2739 |
. . . . 5
⊢
(.r‘𝐹) = (.r‘𝐹) |
11 | | eqid 2739 |
. . . . 5
⊢
(1r‘𝐹) = (1r‘𝐹) |
12 | 4, 5, 6, 7, 8, 9, 10, 11 | lmodlema 19771 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋))) |
13 | 12 | simpld 498 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)))) |
14 | 13 | simp1d 1143 |
. 2
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉) |
15 | 1, 2, 3, 14 | syl3anb 1162 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉) |