| Step | Hyp | Ref
| Expression |
| 1 | | lmodabl 20907 |
. . . 4
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
| 2 | 1 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → 𝑊 ∈ Abel) |
| 3 | | lsmcl.s |
. . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) |
| 4 | 3 | lsssubg 20955 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆) → 𝑇 ∈ (SubGrp‘𝑊)) |
| 5 | 4 | 3adant3 1133 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → 𝑇 ∈ (SubGrp‘𝑊)) |
| 6 | 3 | lsssubg 20955 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 7 | 6 | 3adant2 1132 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 8 | | lsmcl.p |
. . . 4
⊢ ⊕ =
(LSSum‘𝑊) |
| 9 | 8 | lsmsubg2 19877 |
. . 3
⊢ ((𝑊 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝑊)) |
| 10 | 2, 5, 7, 9 | syl3anc 1373 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝑊)) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 12 | 11, 8 | lsmelval 19667 |
. . . . . . 7
⊢ ((𝑇 ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊)) → (𝑢 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑑 ∈ 𝑇 ∃𝑒 ∈ 𝑈 𝑢 = (𝑑(+g‘𝑊)𝑒))) |
| 13 | 5, 7, 12 | syl2anc 584 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑢 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑑 ∈ 𝑇 ∃𝑒 ∈ 𝑈 𝑢 = (𝑑(+g‘𝑊)𝑒))) |
| 14 | 13 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) → (𝑢 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑑 ∈ 𝑇 ∃𝑒 ∈ 𝑈 𝑢 = (𝑑(+g‘𝑊)𝑒))) |
| 15 | | simpll1 1213 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑊 ∈ LMod) |
| 16 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑎 ∈ (Base‘(Scalar‘𝑊))) |
| 17 | | simpll2 1214 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑇 ∈ 𝑆) |
| 18 | | simprl 771 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑑 ∈ 𝑇) |
| 19 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 20 | 19, 3 | lssel 20935 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝑆 ∧ 𝑑 ∈ 𝑇) → 𝑑 ∈ (Base‘𝑊)) |
| 21 | 17, 18, 20 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑑 ∈ (Base‘𝑊)) |
| 22 | | simpll3 1215 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑈 ∈ 𝑆) |
| 23 | | simprr 773 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑒 ∈ 𝑈) |
| 24 | 19, 3 | lssel 20935 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑒 ∈ 𝑈) → 𝑒 ∈ (Base‘𝑊)) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑒 ∈ (Base‘𝑊)) |
| 26 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 27 | | eqid 2737 |
. . . . . . . . . 10
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 28 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 29 | 19, 11, 26, 27, 28 | lmodvsdi 20883 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑑 ∈ (Base‘𝑊) ∧ 𝑒 ∈ (Base‘𝑊))) → (𝑎( ·𝑠
‘𝑊)(𝑑(+g‘𝑊)𝑒)) = ((𝑎( ·𝑠
‘𝑊)𝑑)(+g‘𝑊)(𝑎( ·𝑠
‘𝑊)𝑒))) |
| 30 | 15, 16, 21, 25, 29 | syl13anc 1374 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑊)(𝑑(+g‘𝑊)𝑒)) = ((𝑎( ·𝑠
‘𝑊)𝑑)(+g‘𝑊)(𝑎( ·𝑠
‘𝑊)𝑒))) |
| 31 | 15, 17, 4 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑇 ∈ (SubGrp‘𝑊)) |
| 32 | 15, 22, 6 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 33 | 26, 27, 28, 3 | lssvscl 20953 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑑 ∈ 𝑇)) → (𝑎( ·𝑠
‘𝑊)𝑑) ∈ 𝑇) |
| 34 | 15, 17, 16, 18, 33 | syl22anc 839 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑊)𝑑) ∈ 𝑇) |
| 35 | 26, 27, 28, 3 | lssvscl 20953 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑒 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑊)𝑒) ∈ 𝑈) |
| 36 | 15, 22, 16, 23, 35 | syl22anc 839 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑊)𝑒) ∈ 𝑈) |
| 37 | 11, 8 | lsmelvali 19668 |
. . . . . . . . 9
⊢ (((𝑇 ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊)) ∧ ((𝑎( ·𝑠
‘𝑊)𝑑) ∈ 𝑇 ∧ (𝑎( ·𝑠
‘𝑊)𝑒) ∈ 𝑈)) → ((𝑎( ·𝑠
‘𝑊)𝑑)(+g‘𝑊)(𝑎( ·𝑠
‘𝑊)𝑒)) ∈ (𝑇 ⊕ 𝑈)) |
| 38 | 31, 32, 34, 36, 37 | syl22anc 839 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → ((𝑎( ·𝑠
‘𝑊)𝑑)(+g‘𝑊)(𝑎( ·𝑠
‘𝑊)𝑒)) ∈ (𝑇 ⊕ 𝑈)) |
| 39 | 30, 38 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑊)(𝑑(+g‘𝑊)𝑒)) ∈ (𝑇 ⊕ 𝑈)) |
| 40 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑢 = (𝑑(+g‘𝑊)𝑒) → (𝑎( ·𝑠
‘𝑊)𝑢) = (𝑎( ·𝑠
‘𝑊)(𝑑(+g‘𝑊)𝑒))) |
| 41 | 40 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑢 = (𝑑(+g‘𝑊)𝑒) → ((𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈) ↔ (𝑎( ·𝑠
‘𝑊)(𝑑(+g‘𝑊)𝑒)) ∈ (𝑇 ⊕ 𝑈))) |
| 42 | 39, 41 | syl5ibrcom 247 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈)) → (𝑢 = (𝑑(+g‘𝑊)𝑒) → (𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈))) |
| 43 | 42 | rexlimdvva 3213 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) → (∃𝑑 ∈ 𝑇 ∃𝑒 ∈ 𝑈 𝑢 = (𝑑(+g‘𝑊)𝑒) → (𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈))) |
| 44 | 14, 43 | sylbid 240 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊))) → (𝑢 ∈ (𝑇 ⊕ 𝑈) → (𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈))) |
| 45 | 44 | impr 454 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑢 ∈ (𝑇 ⊕ 𝑈))) → (𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈)) |
| 46 | 45 | ralrimivva 3202 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → ∀𝑎 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (𝑇 ⊕ 𝑈)(𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈)) |
| 47 | 26, 28, 19, 27, 3 | islss4 20960 |
. . 3
⊢ (𝑊 ∈ LMod → ((𝑇 ⊕ 𝑈) ∈ 𝑆 ↔ ((𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝑊) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (𝑇 ⊕ 𝑈)(𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈)))) |
| 48 | 47 | 3ad2ant1 1134 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → ((𝑇 ⊕ 𝑈) ∈ 𝑆 ↔ ((𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝑊) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑊))∀𝑢 ∈ (𝑇 ⊕ 𝑈)(𝑎( ·𝑠
‘𝑊)𝑢) ∈ (𝑇 ⊕ 𝑈)))) |
| 49 | 10, 46, 48 | mpbir2and 713 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) ∈ 𝑆) |