Metamath Proof Explorer

Theorem cnmsubglem

Description: Lemma for rpmsubg and friends. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypotheses cnmgpabl.m 
|- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
cnmsubglem.1 
|- ( x e. A -> x e. CC )
cnmsubglem.2 
|- ( x e. A -> x =/= 0 )
cnmsubglem.3 
|- ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )
cnmsubglem.4 
|- 1 e. A
cnmsubglem.5 
|- ( x e. A -> ( 1 / x ) e. A )
Assertion cnmsubglem 
|- A e. ( SubGrp ` M )

Proof

Step Hyp Ref Expression
1 cnmgpabl.m 
 |-  M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
2 cnmsubglem.1 
 |-  ( x e. A -> x e. CC )
3 cnmsubglem.2 
 |-  ( x e. A -> x =/= 0 )
4 cnmsubglem.3 
 |-  ( ( x e. A /\ y e. A ) -> ( x x. y ) e. A )
5 cnmsubglem.4 
 |-  1 e. A
6 cnmsubglem.5 
 |-  ( x e. A -> ( 1 / x ) e. A )
7 eldifsn 
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
8 2 3 7 sylanbrc 
 |-  ( x e. A -> x e. ( CC \ { 0 } ) )
9 8 ssriv 
 |-  A C_ ( CC \ { 0 } )
10 5 ne0ii 
 |-  A =/= (/)
11 4 ralrimiva 
 |-  ( x e. A -> A. y e. A ( x x. y ) e. A )
12 cnfldinv 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( ( invr ` CCfld ) ` x ) = ( 1 / x ) )
13 2 3 12 syl2anc 
 |-  ( x e. A -> ( ( invr ` CCfld ) ` x ) = ( 1 / x ) )
14 13 6 eqeltrd 
 |-  ( x e. A -> ( ( invr ` CCfld ) ` x ) e. A )
15 11 14 jca 
 |-  ( x e. A -> ( A. y e. A ( x x. y ) e. A /\ ( ( invr ` CCfld ) ` x ) e. A ) )
16 15 rgen 
 |-  A. x e. A ( A. y e. A ( x x. y ) e. A /\ ( ( invr ` CCfld ) ` x ) e. A )
17 1 cnmgpabl 
 |-  M e. Abel
18 ablgrp 
 |-  ( M e. Abel -> M e. Grp )
19 difss 
 |-  ( CC \ { 0 } ) C_ CC
20 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
21 cnfldbas 
 |-  CC = ( Base ` CCfld )
22 20 21 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
23 1 22 ressbas2 
 |-  ( ( CC \ { 0 } ) C_ CC -> ( CC \ { 0 } ) = ( Base ` M ) )
24 19 23 ax-mp 
 |-  ( CC \ { 0 } ) = ( Base ` M )
25 cnex 
 |-  CC e. _V
26 difexg 
 |-  ( CC e. _V -> ( CC \ { 0 } ) e. _V )
27 cnfldmul 
 |-  x. = ( .r ` CCfld )
28 20 27 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
29 1 28 ressplusg 
 |-  ( ( CC \ { 0 } ) e. _V -> x. = ( +g ` M ) )
30 25 26 29 mp2b 
 |-  x. = ( +g ` M )
31 cnfld0 
 |-  0 = ( 0g ` CCfld )
32 cndrng 
 |-  CCfld e. DivRing
33 21 31 32 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
34 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
35 33 1 34 invrfval 
 |-  ( invr ` CCfld ) = ( invg ` M )
36 24 30 35 issubg2 
 |-  ( M e. Grp -> ( A e. ( SubGrp ` M ) <-> ( A C_ ( CC \ { 0 } ) /\ A =/= (/) /\ A. x e. A ( A. y e. A ( x x. y ) e. A /\ ( ( invr ` CCfld ) ` x ) e. A ) ) ) )
37 17 18 36 mp2b 
 |-  ( A e. ( SubGrp ` M ) <-> ( A C_ ( CC \ { 0 } ) /\ A =/= (/) /\ A. x e. A ( A. y e. A ( x x. y ) e. A /\ ( ( invr ` CCfld ) ` x ) e. A ) ) )
38 9 10 16 37 mpbir3an 
 |-  A e. ( SubGrp ` M )