Theorem cnsubrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014)

	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	cnsubrglem	|- 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 )