Metamath Proof Explorer

Theorem lsmcl

Description: The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsmcl.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
Assertion lsmcl ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lsmcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lsmcl.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
4 3 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑊 ∈ Abel )
5 1 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
6 5 3adant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
7 1 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
8 7 3adant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
9 2 lsmsubg2 ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) )
10 4 6 8 9 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) )
11 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
12 11 2 lsmelval ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑑 ∈ 𝑇 ∃ 𝑒 ∈ 𝑈 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) )
13 6 8 12 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑑 ∈ 𝑇 ∃ 𝑒 ∈ 𝑈 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) )
14 13 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑑 ∈ 𝑇 ∃ 𝑒 ∈ 𝑈 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) )
15 simpll1 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
16 simplr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 simpll2 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑇 ∈ 𝑆 )
18 simprl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑑 ∈ 𝑇 )
19 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
20 19 1 lssel ⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑑 ∈ 𝑇 ) → 𝑑 ∈ ( Base ‘ 𝑊 ) )
21 17 18 20 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑑 ∈ ( Base ‘ 𝑊 ) )
22 simpll3 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
23 simprr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑒 ∈ 𝑈 )
24 19 1 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑒 ∈ 𝑈 ) → 𝑒 ∈ ( Base ‘ 𝑊 ) )
25 22 23 24 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑒 ∈ ( Base ‘ 𝑊 ) )
26 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
27 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
28 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
29 19 11 26 27 28 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑑 ∈ ( Base ‘ 𝑊 ) ∧ 𝑒 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ( +g ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) )
30 15 16 21 25 29 syl13anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ( +g ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) )
31 15 17 5 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
32 15 22 7 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
33 26 27 28 1 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑑 ∈ 𝑇 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ∈ 𝑇 )
34 15 17 16 18 33 syl22anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ∈ 𝑇 )
35 26 27 28 1 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑒 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ∈ 𝑈 )
36 15 22 16 23 35 syl22anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ∈ 𝑈 )
37 11 2 lsmelvali ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ∈ 𝑇 ∧ ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ∈ 𝑈 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ( +g ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
38 31 32 34 36 37 syl22anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑑 ) ( +g ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑒 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
39 30 38 eqeltrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
40 oveq2 ⊢ ( 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) = ( 𝑎 ( ·𝑠 ‘ 𝑊 ) ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) )
41 40 eleq1d ⊢ ( 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑎 ( ·𝑠 ‘ 𝑊 ) ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
42 39 41 syl5ibrcom ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑑 ∈ 𝑇 ∧ 𝑒 ∈ 𝑈 ) ) → ( 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
43 42 rexlimdvva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ∃ 𝑑 ∈ 𝑇 ∃ 𝑒 ∈ 𝑈 𝑢 = ( 𝑑 ( +g ‘ 𝑊 ) 𝑒 ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
44 14 43 sylbid ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
45 44 impr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
46 45 ralrimivva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
47 26 28 19 27 1 islss4 ⊢ ( 𝑊 ∈ LMod → ( ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 ↔ ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) )
48 47 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 ↔ ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑢 ∈ ( 𝑇 ⊕ 𝑈 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑢 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) )
49 10 46 48 mpbir2and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )