This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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