Theorem smndlsmidm

Description: The direct product is idempotent for submonoids. (Contributed by AV, 27-Dec-2023)

	Ref	Expression
Hypothesis	lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	smndlsmidm	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		elfvdm	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ dom SubMnd )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	3	submss	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
5		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6	3 5 1	lsmvalx	⊢ ( ( 𝐺 ∈ dom SubMnd ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑈 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
7	2 4 4 6	syl3anc	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
8	5	submcl	⊢ ( ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 )
9	8	3expb	⊢ ( ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 )
10	9	ralrimivva	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 )
11		eqid	⊢ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
12	11	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 ↔ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : ( 𝑈 × 𝑈 ) ⟶ 𝑈 )
13	10 12	sylib	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : ( 𝑈 × 𝑈 ) ⟶ 𝑈 )
14	13	frnd	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ran ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝑈 )
15	7 14	eqsstrd	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) ⊆ 𝑈 )
16	3 1	lsmub1x	⊢ ( ( 𝑈 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑈 ⊕ 𝑈 ) )
17	4 16	mpancom	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → 𝑈 ⊆ ( 𝑈 ⊕ 𝑈 ) )
18	15 17	eqssd	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 )