Theorem cnsubglem

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 )
	cnsubglem.4	|- B e. A
Assertion	cnsubglem	|- A e. ( SubGrp ` 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		cnsubglem.4	|- B e. A
5	1	ssriv	|- A C_ CC
6	4	ne0ii	|- A =/= (/)
7	2	ralrimiva	|- ( x e. A -> A. y e. A ( x + y ) e. A )
8		cnfldneg	|- ( x e. CC -> ( ( invg ` CCfld ) ` x ) = -u x )
9	1 8	syl	|- ( x e. A -> ( ( invg ` CCfld ) ` x ) = -u x )
10	9 3	eqeltrd	|- ( x e. A -> ( ( invg ` CCfld ) ` x ) e. A )
11	7 10	jca	|- ( x e. A -> ( A. y e. A ( x + y ) e. A /\ ( ( invg ` CCfld ) ` x ) e. A ) )
12	11	rgen	|- A. x e. A ( A. y e. A ( x + y ) e. A /\ ( ( invg ` CCfld ) ` x ) e. A )
13		cnring	|- CCfld e. Ring
14		ringgrp	|- ( CCfld e. Ring -> CCfld e. Grp )
15		cnfldbas	|- CC = ( Base ` CCfld )
16		cnfldadd	|- + = ( +g ` CCfld )
17		eqid	|- ( invg ` CCfld ) = ( invg ` CCfld )
18	15 16 17	issubg2	|- ( CCfld e. Grp -> ( A e. ( SubGrp ` CCfld ) <-> ( A C_ CC /\ A =/= (/) /\ A. x e. A ( A. y e. A ( x + y ) e. A /\ ( ( invg ` CCfld ) ` x ) e. A ) ) ) )
19	13 14 18	mp2b	|- ( A e. ( SubGrp ` CCfld ) <-> ( A C_ CC /\ A =/= (/) /\ A. x e. A ( A. y e. A ( x + y ) e. A /\ ( ( invg ` CCfld ) ` x ) e. A ) ) )
20	5 6 12 19	mpbir3an	|- A e. ( SubGrp ` CCfld )