idomsubr

Description: Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025)

		Ref	Expression
	Hypothesis	idomsubr.1	$⊢ φ \to R \in IDomn$
	Assertion	idomsubr	$⊢ φ \to \exists f \in Field \exists s \in SubRing (f) R ≃_{𝑟} (f ↾_{𝑠} s)$

Proof

Step	Hyp	Ref	Expression
1		idomsubr.1	$⊢ φ \to R \in IDomn$
2		fveq2	$⊢ f = Frac (R) \to SubRing (f) = SubRing (Frac (R))$
3		oveq1	$⊢ f = Frac (R) \to f ↾_{𝑠} s = Frac (R) ↾_{𝑠} s$
4	3	breq2d	$⊢ f = Frac (R) \to (R ≃_{𝑟} (f ↾_{𝑠} s) \leftrightarrow R ≃_{𝑟} (Frac (R) ↾_{𝑠} s))$
5	2 4	rexeqbidv	$⊢ f = Frac (R) \to (\exists s \in SubRing (f) R ≃_{𝑟} (f ↾_{𝑠} s) \leftrightarrow \exists s \in SubRing (Frac (R)) R ≃_{𝑟} (Frac (R) ↾_{𝑠} s))$
6	1	fracfld	$⊢ φ \to Frac (R) \in Field$
7		oveq2	$⊢ s = ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \to Frac (R) ↾_{𝑠} s = Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
8	7	breq2d	$⊢ s = ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \to (R ≃_{𝑟} (Frac (R) ↾_{𝑠} s) \leftrightarrow R ≃_{𝑟} (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))))$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ RLReg (R) = RLReg (R)$
11		eqid	$⊢ 1_{R} = 1_{R}$
12	1	idomcringd	$⊢ φ \to R \in CRing$
13		eqid	$⊢ R ~_{RL} RLReg (R) = R ~_{RL} RLReg (R)$
14		opeq1	$⊢ x = y \to ⟨x, 1_{R}⟩ = ⟨y, 1_{R}⟩$
15	14	eceq1d	$⊢ x = y \to [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨y, 1_{R}⟩] (R ~_{RL} RLReg (R))$
16	15	cbvmptv	$⊢ (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) = (y \in {Base}_{R} ⟼ [⟨y, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
17	9 10 11 12 13 16	fracf1	$⊢ φ \to ((x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1}{⟶} ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)) \land (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom Frac (R)))$
18		rnrhmsubrg	$⊢ (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom Frac (R)) \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in SubRing (Frac (R))$
19	17 18	simpl2im	$⊢ φ \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in SubRing (Frac (R))$
20		ssidd	$⊢ φ \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \subseteq ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
21	17	simprd	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom Frac (R))$
22		eqid	$⊢ Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) = Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
23	22	resrhm2b	$⊢ (ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in SubRing (Frac (R)) \land ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \subseteq ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))) \to ((x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom Frac (R)) \leftrightarrow (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))))$
24	23	biimpa	$⊢ ((ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in SubRing (Frac (R)) \land ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \subseteq ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))) \land (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom Frac (R))) \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))))$
25	19 20 21 24	syl21anc	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))))$
26	17	simpld	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1}{⟶} ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))$
27		f1f1orn	$⊢ (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1}{⟶} ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)) \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1 onto}{⟶} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
28	26 27	syl	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1 onto}{⟶} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
29		f1f	$⊢ (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1}{⟶} ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)) \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} ⟶ ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))$
30	26 29	syl	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} ⟶ ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))$
31	30	frnd	$⊢ φ \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \subseteq ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))$
32		eqid	$⊢ Frac (R) = Frac (R)$
33	9 10 32 13	fracbas	$⊢ ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)) = {Base}_{Frac (R)}$
34	31 33	sseqtrdi	$⊢ φ \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \subseteq {Base}_{Frac (R)}$
35		eqid	$⊢ {Base}_{Frac (R)} = {Base}_{Frac (R)}$
36	22 35	ressbas2	$⊢ ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \subseteq {Base}_{Frac (R)} \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) = {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))}$
37	34 36	syl	$⊢ φ \to ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) = {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))}$
38	37	f1oeq3d	$⊢ φ \to ((x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1 onto}{⟶} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \leftrightarrow (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))})$
39	28 38	mpbid	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))}$
40		eqid	$⊢ {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))} = {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))}$
41	9 40	isrim	$⊢ (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingIso (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))) \leftrightarrow ((x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingHom (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))) \land (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{(Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))})$
42	25 39 41	sylanbrc	$⊢ φ \to (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingIso (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R)))))$
43		brrici	$⊢ (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))) \in (R RingIso (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))) \to R ≃_{𝑟} (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))$
44	42 43	syl	$⊢ φ \to R ≃_{𝑟} (Frac (R) ↾_{𝑠} ran (x \in {Base}_{R} ⟼ [⟨x, 1_{R}⟩] (R ~_{RL} RLReg (R))))$
45	8 19 44	rspcedvdw	$⊢ φ \to \exists s \in SubRing (Frac (R)) R ≃_{𝑟} (Frac (R) ↾_{𝑠} s)$
46	5 6 45	rspcedvdw	$⊢ φ \to \exists f \in Field \exists s \in SubRing (f) R ≃_{𝑟} (f ↾_{𝑠} s)$

Metamath Proof Explorer

Theorem idomsubr

Proof