Metamath Proof Explorer


Theorem lsmidmOLD

Description: Obsolete proof of lsmidm as of 13-Jan-2024. Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis lsmub1.p = ( LSSum ‘ 𝐺 )
Assertion lsmidmOLD ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 𝑈 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 lsmub1.p = ( LSSum ‘ 𝐺 )
2 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 eqid ( +g𝐺 ) = ( +g𝐺 )
4 2 3 1 lsmval ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑈 𝑈 ) = ran ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) )
5 4 anidms ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 𝑈 ) = ran ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) )
6 3 subgcl ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑈𝑦𝑈 ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑈 )
7 6 3expb ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥𝑈𝑦𝑈 ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑈 )
8 7 ralrimivva ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑥𝑈𝑦𝑈 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑈 )
9 eqid ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) )
10 9 fmpo ( ∀ 𝑥𝑈𝑦𝑈 ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑈 ↔ ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) : ( 𝑈 × 𝑈 ) ⟶ 𝑈 )
11 8 10 sylib ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) : ( 𝑈 × 𝑈 ) ⟶ 𝑈 )
12 11 frnd ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ran ( 𝑥𝑈 , 𝑦𝑈 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) ⊆ 𝑈 )
13 5 12 eqsstrd ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 𝑈 ) ⊆ 𝑈 )
14 1 lsmub1 ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑈 𝑈 ) )
15 14 anidms ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( 𝑈 𝑈 ) )
16 13 15 eqssd ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 𝑈 ) = 𝑈 )