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

Metamath Proof Explorer

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 )