This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnsubrglemOLD

Description: Obsolete version of cnsubrglem as of 30-Apr-2025. (Contributed by Mario Carneiro, 4-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cnsubglem.1 
|- ( x e. A -> x e. CC )
cnsubglem.2 
|- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )
cnsubglem.3 
|- ( x e. A -> -u x e. A )
cnsubrglem.4 
|- 1 e. A
cnsubrglem.5 
|- ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )
Assertion cnsubrglemOLD 
|- A e. ( SubRing ` CCfld )

Proof

Step Hyp Ref Expression
1 cnsubglem.1 
 |-  ( x e. A -> x e. CC )
2 cnsubglem.2 
 |-  ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )
3 cnsubglem.3 
 |-  ( x e. A -> -u x e. A )
4 cnsubrglem.4 
 |-  1 e. A
5 cnsubrglem.5 
 |-  ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )
6 1 2 3 4 cnsubglem 
 |-  A e. ( SubGrp ` CCfld )
7 5 rgen2 
 |-  A. x e. A A. y e. A ( x x. y ) e. A
8 cnring 
 |-  CCfld e. Ring
9 cnfldbas 
 |-  CC = ( Base ` CCfld )
10 cnfld1 
 |-  1 = ( 1r ` CCfld )
11 cnfldmul 
 |-  x. = ( .r ` CCfld )
12 9 10 11 issubrg2 
 |-  ( CCfld e. Ring -> ( A e. ( SubRing ` CCfld ) <-> ( A e. ( SubGrp ` CCfld ) /\ 1 e. A /\ A. x e. A A. y e. A ( x x. y ) e. A ) ) )
13 8 12 ax-mp 
 |-  ( A e. ( SubRing ` CCfld ) <-> ( A e. ( SubGrp ` CCfld ) /\ 1 e. A /\ A. x e. A A. y e. A ( x x. y ) e. A ) )
14 6 4 7 13 mpbir3an 
 |-  A e. ( SubRing ` CCfld )