Proof of Theorem lssvsubcl
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑊 ∈ LMod) |
2 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
3 | | lssvsubcl.s |
. . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) |
4 | 2, 3 | lssel 18759 |
. . . 4
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑊)) |
5 | 4 | ad2ant2lr 780 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑋 ∈ (Base‘𝑊)) |
6 | 2, 3 | lssel 18759 |
. . . 4
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ (Base‘𝑊)) |
7 | 6 | ad2ant2l 778 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑌 ∈ (Base‘𝑊)) |
8 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑊) = (+g‘𝑊) |
9 | | lssvsubcl.m |
. . . 4
⊢ − =
(-g‘𝑊) |
10 | | eqid 2610 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
11 | | eqid 2610 |
. . . 4
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
12 | | eqid 2610 |
. . . 4
⊢
(invg‘(Scalar‘𝑊)) =
(invg‘(Scalar‘𝑊)) |
13 | | eqid 2610 |
. . . 4
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
14 | 2, 8, 9, 10, 11, 12, 13 | lmodvsubval2 18741 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑌 ∈ (Base‘𝑊)) → (𝑋 − 𝑌) = (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌))) |
15 | 1, 5, 7, 14 | syl3anc 1318 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) = (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌))) |
16 | 10 | lmodfgrp 18695 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
17 | 1, 16 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (Scalar‘𝑊) ∈ Grp) |
18 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
19 | 10, 18, 13 | lmod1cl 18713 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
20 | 1, 19 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
(1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
21 | 18, 12 | grpinvcl 17290 |
. . . . . 6
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))) |
22 | 17, 20, 21 | syl2anc 691 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))) |
23 | 2, 10, 11, 18 | lmodvscl 18703 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))
∧ 𝑌 ∈ (Base‘𝑊)) →
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌) ∈ (Base‘𝑊)) |
24 | 1, 22, 7, 23 | syl3anc 1318 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌) ∈ (Base‘𝑊)) |
25 | 2, 8 | lmodcom 18732 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊) ∧
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌) ∈ (Base‘𝑊)) → (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)) =
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋)) |
26 | 1, 5, 24, 25 | syl3anc 1318 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)) =
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋)) |
27 | | simplr 788 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑈 ∈ 𝑆) |
28 | | simprr 792 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑌 ∈ 𝑈) |
29 | | simprl 790 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑋 ∈ 𝑈) |
30 | 10, 18, 8, 11, 3 | lsscl 18764 |
. . . 4
⊢ ((𝑈 ∈ 𝑆 ∧
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))
∧ 𝑌 ∈ 𝑈 ∧ 𝑋 ∈ 𝑈)) →
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋) ∈ 𝑈) |
31 | 27, 22, 28, 29, 30 | syl13anc 1320 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋) ∈ 𝑈) |
32 | 26, 31 | eqeltrd 2688 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)) ∈ 𝑈) |
33 | 15, 32 | eqeltrd 2688 |
1
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) ∈ 𝑈) |