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 \times B)}$
	isrrext.z	$⊢ Z = ℤMod (R)$
Assertion	isrrext	$⊢ R \in ℝExt \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land (Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D)))$

Proof

Step	Hyp	Ref	Expression
1		isrrext.b	$⊢ B = {Base}_{R}$
2		isrrext.v	$⊢ D = {dist (R) ↾}_{(B \times B)}$
3		isrrext.z	$⊢ Z = ℤMod (R)$
4		elin	$⊢ R \in (NrmRing \cap DivRing) \leftrightarrow (R \in NrmRing \land R \in DivRing)$
5	4	anbi1i	$⊢ (R \in (NrmRing \cap DivRing) \land ((Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D)))) \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land ((Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D))))$
6		fveq2	$⊢ r = R \to ℤMod (r) = ℤMod (R)$
7	6	eleq1d	$⊢ r = R \to (ℤMod (r) \in NrmMod \leftrightarrow ℤMod (R) \in NrmMod)$
8	3	eleq1i	$⊢ Z \in NrmMod \leftrightarrow ℤMod (R) \in NrmMod$
9	7 8	bitr4di	$⊢ r = R \to (ℤMod (r) \in NrmMod \leftrightarrow Z \in NrmMod)$
10		fveqeq2	$⊢ r = R \to (chr (r) = 0 \leftrightarrow chr (R) = 0)$
11	9 10	anbi12d	$⊢ r = R \to ((ℤMod (r) \in NrmMod \land chr (r) = 0) \leftrightarrow (Z \in NrmMod \land chr (R) = 0))$
12		eleq1	$⊢ r = R \to (r \in CUnifSp \leftrightarrow R \in CUnifSp)$
13		fveq2	$⊢ r = R \to UnifSt (r) = UnifSt (R)$
14		fveq2	$⊢ r = R \to dist (r) = dist (R)$
15		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
16	15 1	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
17	16	sqxpeqd	$⊢ r = R \to {Base}_{r} \times {Base}_{r} = B \times B$
18	14 17	reseq12d	$⊢ r = R \to {dist (r) ↾}_{({Base}_{r} \times {Base}_{r})} = {dist (R) ↾}_{(B \times B)}$
19	18 2	eqtr4di	$⊢ r = R \to {dist (r) ↾}_{({Base}_{r} \times {Base}_{r})} = D$
20	19	fveq2d	$⊢ r = R \to metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})}) = metUnif (D)$
21	13 20	eqeq12d	$⊢ r = R \to (UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})}) \leftrightarrow UnifSt (R) = metUnif (D))$
22	12 21	anbi12d	$⊢ r = R \to ((r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})) \leftrightarrow (R \in CUnifSp \land UnifSt (R) = metUnif (D)))$
23	11 22	anbi12d	$⊢ r = R \to (((ℤMod (r) \in NrmMod \land chr (r) = 0) \land (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})}))) \leftrightarrow ((Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D))))$
24		df-rrext	$⊢ ℝExt = \{r \in (NrmRing \cap DivRing) \| ((ℤMod (r) \in NrmMod \land chr (r) = 0) \land (r \in CUnifSp \land UnifSt (r) = metUnif ({dist (r) ↾}_{({Base}_{r} \times {Base}_{r})})))\}$
25	23 24	elrab2	$⊢ R \in ℝExt \leftrightarrow (R \in (NrmRing \cap DivRing) \land ((Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D))))$
26		3anass	$⊢ ((R \in NrmRing \land R \in DivRing) \land (Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D))) \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land ((Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D))))$
27	5 25 26	3bitr4i	$⊢ R \in ℝExt \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land (Z \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif (D)))$

Metamath Proof Explorer

Theorem isrrext

Proof