Metamath Proof Explorer

Theorem submnd0OLD

Description: Obsolete version of submnd0 as of 12-Aug-2026. The zero of a submonoid is the same as the zero in the parent monoid. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses submnd0.b 
|- B = ( Base ` G )
submnd0.z 
|- .0. = ( 0g ` G )
submnd0.h 
|- H = ( G |`s S )
Assertion submnd0OLD 
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> .0. = ( 0g ` H ) )

Proof

Step Hyp Ref Expression
1 submnd0.b 
 |-  B = ( Base ` G )
2 submnd0.z 
 |-  .0. = ( 0g ` G )
3 submnd0.h 
 |-  H = ( G |`s S )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
6 eqid 
 |-  ( +g ` H ) = ( +g ` H )
7 simprr 
 |-  ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> .0. e. S )
8 3 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` H ) )
9 8 ad2antrl 
 |-  ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> S = ( Base ` H ) )
10 7 9 eleqtrd 
 |-  ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> .0. e. ( Base ` H ) )
11 fvex 
 |-  ( Base ` H ) e. _V
12 9 11 eqeltrdi 
 |-  ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> S e. _V )
13 12 adantr 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> S e. _V )
14 eqid 
 |-  ( +g ` G ) = ( +g ` G )
15 3 14 ressplusg 
 |-  ( S e. _V -> ( +g ` G ) = ( +g ` H ) )
16 13 15 syl 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( +g ` G ) = ( +g ` H ) )
17 16 oveqd 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( .0. ( +g ` G ) x ) = ( .0. ( +g ` H ) x ) )
18 simpll 
 |-  ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> G e. Mnd )
19 3 1 ressbasss 
 |-  ( Base ` H ) C_ B
20 19 sseli 
 |-  ( x e. ( Base ` H ) -> x e. B )
21 1 14 2 mndlid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( .0. ( +g ` G ) x ) = x )
22 18 20 21 syl2an 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( .0. ( +g ` G ) x ) = x )
23 17 22 eqtr3d 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( .0. ( +g ` H ) x ) = x )
24 16 oveqd 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( x ( +g ` G ) .0. ) = ( x ( +g ` H ) .0. ) )
25 1 14 2 mndrid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( x ( +g ` G ) .0. ) = x )
26 18 20 25 syl2an 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( x ( +g ` G ) .0. ) = x )
27 24 26 eqtr3d 
 |-  ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) /\ x e. ( Base ` H ) ) -> ( x ( +g ` H ) .0. ) = x )
28 4 5 6 10 23 27 ismgmid2 
 |-  ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> .0. = ( 0g ` H ) )