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 ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 )