Metamath Proof Explorer

Theorem lsssubg

Description: All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014)

Ref Expression
Hypothesis lsssubg.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lsssubg ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 lsssubg.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3 2 1 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
4 3 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
5 1 lssn0 ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ≠ ∅ )
6 5 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ≠ ∅ )
7 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
8 7 1 lssvacl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
9 8 anassrs ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
10 9 ralrimiva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 )
11 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
12 1 11 lssvnegcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ 𝑈 )
13 12 3expa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ 𝑈 )
14 10 13 jca ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → ( ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ 𝑈 ) )
15 14 ralrimiva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑈 ( ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ 𝑈 ) )
16 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
17 16 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑊 ∈ Grp )
18 2 7 11 issubg2 ⊢ ( 𝑊 ∈ Grp → ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ↔ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ 𝑈 ) ) ) )
19 17 18 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ↔ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ∈ 𝑈 ∧ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ∈ 𝑈 ) ) ) )
20 4 6 15 19 mpbir3and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )