Metamath Proof Explorer

Theorem submnd0

Description: The zero of a submonoid is the same as the zero in the parent monoid. (Note that we must add the condition that the zero of the parent monoid is actually contained in the submonoid, because it is possible to have "subsets that are monoids" which are not submonoids because they have a different identity element. See, for example, smndex1mnd and smndex1n0mnd ). (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses submnd0.b 
|- B = ( Base ` G )
submnd0.z 
|- .0. = ( 0g ` G )
submnd0.h 
|- H = ( G |`s S )
Assertion submnd0 
|- ( ( ( 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 ) )