Metamath Proof Explorer

Theorem isrrext

Description: Express the property " R is an extension of RR ". (Contributed by Thierry Arnoux, 2-May-2018)

Ref Expression
Hypotheses isrrext.b 
|- B = ( Base ` R )
isrrext.v 
|- D = ( ( dist ` R ) |` ( B X. B ) )
isrrext.z 
|- Z = ( ZMod ` R )
Assertion isrrext 
|- ( R e. RRExt <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) )

Proof

Step Hyp Ref Expression
1 isrrext.b 
 |-  B = ( Base ` R )
2 isrrext.v 
 |-  D = ( ( dist ` R ) |` ( B X. B ) )
3 isrrext.z 
 |-  Z = ( ZMod ` R )
4 elin 
 |-  ( R e. ( NrmRing i^i DivRing ) <-> ( R e. NrmRing /\ R e. DivRing ) )
5 4 anbi1i 
 |-  ( ( R e. ( NrmRing i^i DivRing ) /\ ( ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) ) <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) ) )
6 fveq2 
 |-  ( r = R -> ( ZMod ` r ) = ( ZMod ` R ) )
7 6 eleq1d 
 |-  ( r = R -> ( ( ZMod ` r ) e. NrmMod <-> ( ZMod ` R ) e. NrmMod ) )
8 3 eleq1i 
 |-  ( Z e. NrmMod <-> ( ZMod ` R ) e. NrmMod )
9 7 8 bitr4di 
 |-  ( r = R -> ( ( ZMod ` r ) e. NrmMod <-> Z e. NrmMod ) )
10 fveqeq2 
 |-  ( r = R -> ( ( chr ` r ) = 0 <-> ( chr ` R ) = 0 ) )
11 9 10 anbi12d 
 |-  ( r = R -> ( ( ( ZMod ` r ) e. NrmMod /\ ( chr ` r ) = 0 ) <-> ( Z e. NrmMod /\ ( chr ` R ) = 0 ) ) )
12 eleq1 
 |-  ( r = R -> ( r e. CUnifSp <-> R e. CUnifSp ) )
13 fveq2 
 |-  ( r = R -> ( UnifSt ` r ) = ( UnifSt ` R ) )
14 fveq2 
 |-  ( r = R -> ( dist ` r ) = ( dist ` R ) )
15 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
16 15 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
17 16 sqxpeqd 
 |-  ( r = R -> ( ( Base ` r ) X. ( Base ` r ) ) = ( B X. B ) )
18 14 17 reseq12d 
 |-  ( r = R -> ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) = ( ( dist ` R ) |` ( B X. B ) ) )
19 18 2 eqtr4di 
 |-  ( r = R -> ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) = D )
20 19 fveq2d 
 |-  ( r = R -> ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) = ( metUnif ` D ) )
21 13 20 eqeq12d 
 |-  ( r = R -> ( ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) <-> ( UnifSt ` R ) = ( metUnif ` D ) ) )
22 12 21 anbi12d 
 |-  ( r = R -> ( ( r e. CUnifSp /\ ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) <-> ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) )
23 11 22 anbi12d 
 |-  ( r = R -> ( ( ( ( ZMod ` r ) e. NrmMod /\ ( chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) ) <-> ( ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) ) )
24 df-rrext 
 |-  RRExt = { r e. ( NrmRing i^i DivRing ) | ( ( ( ZMod ` r ) e. NrmMod /\ ( chr ` r ) = 0 ) /\ ( r e. CUnifSp /\ ( UnifSt ` r ) = ( metUnif ` ( ( dist ` r ) |` ( ( Base ` r ) X. ( Base ` r ) ) ) ) ) ) }
25 23 24 elrab2 
 |-  ( R e. RRExt <-> ( R e. ( NrmRing i^i DivRing ) /\ ( ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) ) )
26 3anass 
 |-  ( ( ( R e. NrmRing /\ R e. DivRing ) /\ ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) ) )
27 5 25 26 3bitr4i 
 |-  ( R e. RRExt <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` D ) ) ) )