Metamath Proof Explorer

Theorem ringidss

Description: A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses ringidss.g 
|- M = ( ( mulGrp ` R ) |`s A )
ringidss.b 
|- B = ( Base ` R )
ringidss.u 
|- .1. = ( 1r ` R )
Assertion ringidss 
|- ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> .1. = ( 0g ` M ) )

Proof

Step Hyp Ref Expression
1 ringidss.g 
 |-  M = ( ( mulGrp ` R ) |`s A )
2 ringidss.b 
 |-  B = ( Base ` R )
3 ringidss.u 
 |-  .1. = ( 1r ` R )
4 eqid 
 |-  ( Base ` M ) = ( Base ` M )
5 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
6 eqid 
 |-  ( +g ` M ) = ( +g ` M )
7 simp3 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> .1. e. A )
8 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 8 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
10 1 9 ressbas2 
 |-  ( A C_ B -> A = ( Base ` M ) )
11 10 3ad2ant2 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> A = ( Base ` M ) )
12 7 11 eleqtrd 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> .1. e. ( Base ` M ) )
13 simp2 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> A C_ B )
14 11 13 eqsstrrd 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> ( Base ` M ) C_ B )
15 14 sselda 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. ( Base ` M ) ) -> y e. B )
16 fvex 
 |-  ( Base ` M ) e. _V
17 11 16 eqeltrdi 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> A e. _V )
18 eqid 
 |-  ( .r ` R ) = ( .r ` R )
19 8 18 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
20 1 19 ressplusg 
 |-  ( A e. _V -> ( .r ` R ) = ( +g ` M ) )
21 17 20 syl 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> ( .r ` R ) = ( +g ` M ) )
22 21 adantr 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( .r ` R ) = ( +g ` M ) )
23 22 oveqd 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( .1. ( .r ` R ) y ) = ( .1. ( +g ` M ) y ) )
24 2 18 3 ringlidm 
 |-  ( ( R e. Ring /\ y e. B ) -> ( .1. ( .r ` R ) y ) = y )
25 24 3ad2antl1 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( .1. ( .r ` R ) y ) = y )
26 23 25 eqtr3d 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( .1. ( +g ` M ) y ) = y )
27 15 26 syldan 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. ( Base ` M ) ) -> ( .1. ( +g ` M ) y ) = y )
28 22 oveqd 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( y ( .r ` R ) .1. ) = ( y ( +g ` M ) .1. ) )
29 2 18 3 ringridm 
 |-  ( ( R e. Ring /\ y e. B ) -> ( y ( .r ` R ) .1. ) = y )
30 29 3ad2antl1 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( y ( .r ` R ) .1. ) = y )
31 28 30 eqtr3d 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. B ) -> ( y ( +g ` M ) .1. ) = y )
32 15 31 syldan 
 |-  ( ( ( R e. Ring /\ A C_ B /\ .1. e. A ) /\ y e. ( Base ` M ) ) -> ( y ( +g ` M ) .1. ) = y )
33 4 5 6 12 27 32 ismgmid2 
 |-  ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> .1. = ( 0g ` M ) )