Metamath Proof Explorer

Theorem cnsubrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

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 1 adantr 
 |-  ( ( x e. A /\ y e. A ) -> x e. CC )
8 1 ax-gen 
 |-  A. x ( x e. A -> x e. CC )
9 eleq1 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
10 eleq1 
 |-  ( x = y -> ( x e. CC <-> y e. CC ) )
11 9 10 imbi12d 
 |-  ( x = y -> ( ( x e. A -> x e. CC ) <-> ( y e. A -> y e. CC ) ) )
12 11 spvv 
 |-  ( A. x ( x e. A -> x e. CC ) -> ( y e. A -> y e. CC ) )
13 8 12 ax-mp 
 |-  ( y e. A -> y e. CC )
14 13 adantl 
 |-  ( ( x e. A /\ y e. A ) -> y e. CC )
15 7 14 jca 
 |-  ( ( x e. A /\ y e. A ) -> ( x e. CC /\ y e. CC ) )
16 ovmpot 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( x x. y ) )
17 15 16 syl 
 |-  ( ( x e. A /\ y e. A ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( x x. y ) )
18 17 eqcomd 
 |-  ( ( x e. A /\ y e. A ) -> ( x x. y ) = ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
19 18 eleq1d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( x x. y ) e. A <-> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. A ) )
20 5 19 mpbid 
 |-  ( ( x e. A /\ y e. A ) -> ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. A )
21 20 rgen2 
 |-  A. x e. A A. y e. A ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. A
22 cnring 
 |-  CCfld e. Ring
23 cnfldbas 
 |-  CC = ( Base ` CCfld )
24 cnfld1 
 |-  1 = ( 1r ` CCfld )
25 mpocnfldmul 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld )
26 23 24 25 issubrg2 
 |-  ( CCfld e. Ring -> ( A e. ( SubRing ` CCfld ) <-> ( A e. ( SubGrp ` CCfld ) /\ 1 e. A /\ A. x e. A A. y e. A ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. A ) ) )
27 22 26 ax-mp 
 |-  ( A e. ( SubRing ` CCfld ) <-> ( A e. ( SubGrp ` CCfld ) /\ 1 e. A /\ A. x e. A A. y e. A ( x ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. A ) )
28 6 4 21 27 mpbir3an 
 |-  A e. ( SubRing ` CCfld )