Proof of Theorem lssvsubcl
| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑊 ∈ LMod) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 3 | | lssvsubcl.s |
. . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) |
| 4 | 2, 3 | lssel 20935 |
. . . 4
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑊)) |
| 5 | 4 | ad2ant2lr 748 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑋 ∈ (Base‘𝑊)) |
| 6 | 2, 3 | lssel 20935 |
. . . 4
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ (Base‘𝑊)) |
| 7 | 6 | ad2ant2l 746 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑌 ∈ (Base‘𝑊)) |
| 8 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 9 | | lssvsubcl.m |
. . . 4
⊢ − =
(-g‘𝑊) |
| 10 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 11 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 12 | | eqid 2737 |
. . . 4
⊢
(invg‘(Scalar‘𝑊)) =
(invg‘(Scalar‘𝑊)) |
| 13 | | eqid 2737 |
. . . 4
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
| 14 | 2, 8, 9, 10, 11, 12, 13 | lmodvsubval2 20915 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑌 ∈ (Base‘𝑊)) → (𝑋 − 𝑌) = (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌))) |
| 15 | 1, 5, 7, 14 | syl3anc 1373 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) = (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌))) |
| 16 | 10 | lmodfgrp 20867 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
| 17 | 1, 16 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (Scalar‘𝑊) ∈ Grp) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 19 | 10, 18, 13 | lmod1cl 20887 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
| 20 | 1, 19 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
(1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
| 21 | 18, 12 | grpinvcl 19005 |
. . . . . 6
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))) |
| 22 | 17, 20, 21 | syl2anc 584 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))) |
| 23 | 2, 10, 11, 18 | lmodvscl 20876 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))
∧ 𝑌 ∈ (Base‘𝑊)) →
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌) ∈ (Base‘𝑊)) |
| 24 | 1, 22, 7, 23 | syl3anc 1373 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌) ∈ (Base‘𝑊)) |
| 25 | 2, 8 | lmodcom 20906 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊) ∧
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌) ∈ (Base‘𝑊)) → (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)) =
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋)) |
| 26 | 1, 5, 24, 25 | syl3anc 1373 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)) =
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋)) |
| 27 | | simplr 769 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑈 ∈ 𝑆) |
| 28 | | simprr 773 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑌 ∈ 𝑈) |
| 29 | | simprl 771 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → 𝑋 ∈ 𝑈) |
| 30 | 10, 18, 8, 11, 3 | lsscl 20940 |
. . . 4
⊢ ((𝑈 ∈ 𝑆 ∧
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈
(Base‘(Scalar‘𝑊))
∧ 𝑌 ∈ 𝑈 ∧ 𝑋 ∈ 𝑈)) →
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋) ∈ 𝑈) |
| 31 | 27, 22, 28, 29, 30 | syl13anc 1374 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) →
((((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)(+g‘𝑊)𝑋) ∈ 𝑈) |
| 32 | 26, 31 | eqeltrd 2841 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋(+g‘𝑊)(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑌)) ∈ 𝑈) |
| 33 | 15, 32 | eqeltrd 2841 |
1
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈)) → (𝑋 − 𝑌) ∈ 𝑈) |