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 ` G )
Assertion smndlsmidm 
|- ( U e. ( SubMnd ` G ) -> ( U .(+) U ) = U )

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 elfvdm 
 |-  ( U e. ( SubMnd ` G ) -> G e. dom SubMnd )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 3 submss 
 |-  ( U e. ( SubMnd ` G ) -> U C_ ( Base ` G ) )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 3 5 1 lsmvalx 
 |-  ( ( G e. dom SubMnd /\ U C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( U .(+) U ) = ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) )
7 2 4 4 6 syl3anc 
 |-  ( U e. ( SubMnd ` G ) -> ( U .(+) U ) = ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) )
8 5 submcl 
 |-  ( ( U e. ( SubMnd ` G ) /\ x e. U /\ y e. U ) -> ( x ( +g ` G ) y ) e. U )
9 8 3expb 
 |-  ( ( U e. ( SubMnd ` G ) /\ ( x e. U /\ y e. U ) ) -> ( x ( +g ` G ) y ) e. U )
10 9 ralrimivva 
 |-  ( U e. ( SubMnd ` G ) -> A. x e. U A. y e. U ( x ( +g ` G ) y ) e. U )
11 eqid 
 |-  ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) = ( x e. U , y e. U |-> ( x ( +g ` G ) y ) )
12 11 fmpo 
 |-  ( A. x e. U A. y e. U ( x ( +g ` G ) y ) e. U <-> ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) : ( U X. U ) --> U )
13 10 12 sylib 
 |-  ( U e. ( SubMnd ` G ) -> ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) : ( U X. U ) --> U )
14 13 frnd 
 |-  ( U e. ( SubMnd ` G ) -> ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) C_ U )
15 7 14 eqsstrd 
 |-  ( U e. ( SubMnd ` G ) -> ( U .(+) U ) C_ U )
16 3 1 lsmub1x 
 |-  ( ( U C_ ( Base ` G ) /\ U e. ( SubMnd ` G ) ) -> U C_ ( U .(+) U ) )
17 4 16 mpancom 
 |-  ( U e. ( SubMnd ` G ) -> U C_ ( U .(+) U ) )
18 15 17 eqssd 
 |-  ( U e. ( SubMnd ` G ) -> ( U .(+) U ) = U )