Metamath Proof Explorer

Theorem issubrngd2

Description: Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014)

Ref Expression
Hypotheses issubrngd.s 
|- ( ph -> S = ( I |`s D ) )
issubrngd.z 
|- ( ph -> .0. = ( 0g ` I ) )
issubrngd.p 
|- ( ph -> .+ = ( +g ` I ) )
issubrngd.ss 
|- ( ph -> D C_ ( Base ` I ) )
issubrngd.zcl 
|- ( ph -> .0. e. D )
issubrngd.acl 
|- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )
issubrngd.ncl 
|- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )
issubrngd.o 
|- ( ph -> .1. = ( 1r ` I ) )
issubrngd.t 
|- ( ph -> .x. = ( .r ` I ) )
issubrngd.ocl 
|- ( ph -> .1. e. D )
issubrngd.tcl 
|- ( ( ph /\ x e. D /\ y e. D ) -> ( x .x. y ) e. D )
issubrngd.g 
|- ( ph -> I e. Ring )
Assertion issubrngd2 
|- ( ph -> D e. ( SubRing ` I ) )

Proof

Step Hyp Ref Expression
1 issubrngd.s 
 |-  ( ph -> S = ( I |`s D ) )
2 issubrngd.z 
 |-  ( ph -> .0. = ( 0g ` I ) )
3 issubrngd.p 
 |-  ( ph -> .+ = ( +g ` I ) )
4 issubrngd.ss 
 |-  ( ph -> D C_ ( Base ` I ) )
5 issubrngd.zcl 
 |-  ( ph -> .0. e. D )
6 issubrngd.acl 
 |-  ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )
7 issubrngd.ncl 
 |-  ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )
8 issubrngd.o 
 |-  ( ph -> .1. = ( 1r ` I ) )
9 issubrngd.t 
 |-  ( ph -> .x. = ( .r ` I ) )
10 issubrngd.ocl 
 |-  ( ph -> .1. e. D )
11 issubrngd.tcl 
 |-  ( ( ph /\ x e. D /\ y e. D ) -> ( x .x. y ) e. D )
12 issubrngd.g 
 |-  ( ph -> I e. Ring )
13 ringgrp 
 |-  ( I e. Ring -> I e. Grp )
14 12 13 syl 
 |-  ( ph -> I e. Grp )
15 1 2 3 4 5 6 7 14 issubgrpd2 
 |-  ( ph -> D e. ( SubGrp ` I ) )
16 8 10 eqeltrrd 
 |-  ( ph -> ( 1r ` I ) e. D )
17 9 oveqdr 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( x .x. y ) = ( x ( .r ` I ) y ) )
18 11 3expb 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( x .x. y ) e. D )
19 17 18 eqeltrrd 
 |-  ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( x ( .r ` I ) y ) e. D )
20 19 ralrimivva 
 |-  ( ph -> A. x e. D A. y e. D ( x ( .r ` I ) y ) e. D )
21 eqid 
 |-  ( Base ` I ) = ( Base ` I )
22 eqid 
 |-  ( 1r ` I ) = ( 1r ` I )
23 eqid 
 |-  ( .r ` I ) = ( .r ` I )
24 21 22 23 issubrg2 
 |-  ( I e. Ring -> ( D e. ( SubRing ` I ) <-> ( D e. ( SubGrp ` I ) /\ ( 1r ` I ) e. D /\ A. x e. D A. y e. D ( x ( .r ` I ) y ) e. D ) ) )
25 12 24 syl 
 |-  ( ph -> ( D e. ( SubRing ` I ) <-> ( D e. ( SubGrp ` I ) /\ ( 1r ` I ) e. D /\ A. x e. D A. y e. D ( x ( .r ` I ) y ) e. D ) ) )
26 15 16 20 25 mpbir3and 
 |-  ( ph -> D e. ( SubRing ` I ) )