rlocf1

Description: The embedding F of a ring R into its localization L . (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocf1.1	$⊢ B = {Base}_{R}$
	rlocf1.2	$⊢ \underset{˙}{1} = 1_{R}$
	rlocf1.3	No typesetting found for \|- L = ( R RLocal S ) with typecode \|-
	rlocf1.4	No typesetting found for \|- .~ = ( R ~RL S ) with typecode \|-
	rlocf1.5	$⊢ F = (x \in B ⟼ [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim})$
	rlocf1.6	$⊢ φ \to R \in CRing$
	rlocf1.7	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
	rlocf1.8	$⊢ φ \to S \subseteq RLReg (R)$
Assertion	rlocf1	$⊢ φ \to (F : B \underset{1-1}{⟶} (B \times S) / \underset{˙}{\sim} \land F \in (R RingHom L))$

Proof

Step	Hyp	Ref	Expression
1		rlocf1.1	$⊢ B = {Base}_{R}$
2		rlocf1.2	$⊢ \underset{˙}{1} = 1_{R}$
3		rlocf1.3	Could not format L = ( R RLocal S ) : No typesetting found for \|- L = ( R RLocal S ) with typecode \|-
4		rlocf1.4	Could not format .~ = ( R ~RL S ) : No typesetting found for \|- .~ = ( R ~RL S ) with typecode \|-
5		rlocf1.5	$⊢ F = (x \in B ⟼ [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim})$
6		rlocf1.6	$⊢ φ \to R \in CRing$
7		rlocf1.7	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
8		rlocf1.8	$⊢ φ \to S \subseteq RLReg (R)$
9		simpr	$⊢ (φ \land x \in B) \to x \in B$
10		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
11	10 2	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
12	11	subm0cl	$⊢ S \in SubMnd ({mulGrp}_{R}) \to \underset{˙}{1} \in S$
13	7 12	syl	$⊢ φ \to \underset{˙}{1} \in S$
14	13	adantr	$⊢ (φ \land x \in B) \to \underset{˙}{1} \in S$
15	9 14	opelxpd	$⊢ (φ \land x \in B) \to ⟨x, \underset{˙}{1}⟩ \in (B \times S)$
16	4	ovexi	$⊢ \underset{˙}{\sim} \in V$
17	16	ecelqsi	$⊢ ⟨x, \underset{˙}{1}⟩ \in (B \times S) \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
18	15 17	syl	$⊢ (φ \land x \in B) \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
19	18	ralrimiva	$⊢ φ \to \forall x \in B [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
20	6	crnggrpd	$⊢ φ \to R \in Grp$
21	20	ad5antr	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to R \in Grp$
22		simp-5r	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to x \in B$
23		simp-4r	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to y \in B$
24		vex	$⊢ x \in V$
25	2	fvexi	$⊢ \underset{˙}{1} \in V$
26	24 25	op1st	$⊢ 1^{st} (⟨x, \underset{˙}{1}⟩) = x$
27	26	a1i	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨x, \underset{˙}{1}⟩) = x$
28		vex	$⊢ y \in V$
29	28 25	op2nd	$⊢ 2^{nd} (⟨y, \underset{˙}{1}⟩) = \underset{˙}{1}$
30	29	a1i	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 2^{nd} (⟨y, \underset{˙}{1}⟩) = \underset{˙}{1}$
31	27 30	oveq12d	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩) = x \cdot_{R} \underset{˙}{1}$
32		eqid	$⊢ \cdot_{R} = \cdot_{R}$
33	6	crngringd	$⊢ φ \to R \in Ring$
34	33	ad5antr	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to R \in Ring$
35	1 32 2 34 22	ringridmd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to x \cdot_{R} \underset{˙}{1} = x$
36	31 35	eqtrd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩) = x$
37	28 25	op1st	$⊢ 1^{st} (⟨y, \underset{˙}{1}⟩) = y$
38	37	a1i	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨y, \underset{˙}{1}⟩) = y$
39	24 25	op2nd	$⊢ 2^{nd} (⟨x, \underset{˙}{1}⟩) = \underset{˙}{1}$
40	39	a1i	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 2^{nd} (⟨x, \underset{˙}{1}⟩) = \underset{˙}{1}$
41	38 40	oveq12d	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩) = y \cdot_{R} \underset{˙}{1}$
42	1 32 2 34 23	ringridmd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to y \cdot_{R} \underset{˙}{1} = y$
43	41 42	eqtrd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩) = y$
44	36 43	oveq12d	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) = x -_{R} y$
45	8	ad5antr	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to S \subseteq RLReg (R)$
46		simplr	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to t \in S$
47	45 46	sseldd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to t \in RLReg (R)$
48	27 22	eqeltrd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨x, \underset{˙}{1}⟩) \in B$
49	10 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
50	49	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq B$
51	7 50	syl	$⊢ φ \to S \subseteq B$
52	51 13	sseldd	$⊢ φ \to \underset{˙}{1} \in B$
53	52	ad5antr	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to \underset{˙}{1} \in B$
54	30 53	eqeltrd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 2^{nd} (⟨y, \underset{˙}{1}⟩) \in B$
55	1 32 34 48 54	ringcld	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩) \in B$
56	38 23	eqeltrd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨y, \underset{˙}{1}⟩) \in B$
57	40 53	eqeltrd	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 2^{nd} (⟨x, \underset{˙}{1}⟩) \in B$
58	1 32 34 56 57	ringcld	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to 1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩) \in B$
59		eqid	$⊢ -_{R} = -_{R}$
60	1 59	grpsubcl	$⊢ (R \in Grp \land 1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩) \in B \land 1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩) \in B) \to (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) \in B$
61	21 55 58 60	syl3anc	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) \in B$
62		simpr	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}$
63		eqid	$⊢ RLReg (R) = RLReg (R)$
64		eqid	$⊢ 0_{R} = 0_{R}$
65	63 1 32 64	rrgeq0i	$⊢ (t \in RLReg (R) \land (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) \in B) \to (t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R} \to (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) = 0_{R})$
66	65	imp	$⊢ ((t \in RLReg (R) \land (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) \in B) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) = 0_{R}$
67	47 61 62 66	syl21anc	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to (1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩)) = 0_{R}$
68	44 67	eqtr3d	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to x -_{R} y = 0_{R}$
69	1 64 59	grpsubeq0	$⊢ (R \in Grp \land x \in B \land y \in B) \to (x -_{R} y = 0_{R} \leftrightarrow x = y)$
70	69	biimpa	$⊢ ((R \in Grp \land x \in B \land y \in B) \land x -_{R} y = 0_{R}) \to x = y$
71	21 22 23 68 70	syl31anc	$⊢ (((((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \land t \in S) \land t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}) \to x = y$
72	51	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \to S \subseteq B$
73		eqid	$⊢ B \times S = B \times S$
74	6	ad2antrr	$⊢ ((φ \land x \in B) \land y \in B) \to R \in CRing$
75	7	ad2antrr	$⊢ ((φ \land x \in B) \land y \in B) \to S \in SubMnd ({mulGrp}_{R})$
76	1 64 2 32 59 73 4 74 75	erler	$⊢ ((φ \land x \in B) \land y \in B) \to \underset{˙}{\sim} Er (B \times S)$
77	15	adantr	$⊢ ((φ \land x \in B) \land y \in B) \to ⟨x, \underset{˙}{1}⟩ \in (B \times S)$
78	76 77	erth	$⊢ ((φ \land x \in B) \land y \in B) \to (⟨x, \underset{˙}{1}⟩ \underset{˙}{\sim} ⟨y, \underset{˙}{1}⟩ \leftrightarrow [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim})$
79	78	biimpar	$⊢ (((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \to ⟨x, \underset{˙}{1}⟩ \underset{˙}{\sim} ⟨y, \underset{˙}{1}⟩$
80	1 4 72 64 32 59 79	erldi	$⊢ (((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \to \exists t \in S t \cdot_{R} ((1^{st} (⟨x, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨y, \underset{˙}{1}⟩)) -_{R} (1^{st} (⟨y, \underset{˙}{1}⟩) \cdot_{R} 2^{nd} (⟨x, \underset{˙}{1}⟩))) = 0_{R}$
81	71 80	r19.29a	$⊢ (((φ \land x \in B) \land y \in B) \land [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}) \to x = y$
82	81	ex	$⊢ ((φ \land x \in B) \land y \in B) \to ([⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim} \to x = y)$
83	82	anasss	$⊢ (φ \land (x \in B \land y \in B)) \to ([⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim} \to x = y)$
84	83	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B ([⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim} \to x = y)$
85		opeq1	$⊢ x = y \to ⟨x, \underset{˙}{1}⟩ = ⟨y, \underset{˙}{1}⟩$
86	85	eceq1d	$⊢ x = y \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim}$
87	5 86	f1mpt	$⊢ F : B \underset{1-1}{⟶} (B \times S) / \underset{˙}{\sim} \leftrightarrow (\forall x \in B [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim}) \land \forall x \in B \forall y \in B ([⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨y, \underset{˙}{1}⟩] \underset{˙}{\sim} \to x = y))$
88	19 84 87	sylanbrc	$⊢ φ \to F : B \underset{1-1}{⟶} (B \times S) / \underset{˙}{\sim}$
89		eqid	$⊢ 1_{L} = 1_{L}$
90		eqid	$⊢ \cdot_{L} = \cdot_{L}$
91		eqid	$⊢ +_{R} = +_{R}$
92	1 32 91 3 4 6 7	rloccring	$⊢ φ \to L \in CRing$
93	92	crngringd	$⊢ φ \to L \in Ring$
94		opeq1	$⊢ x = \underset{˙}{1} \to ⟨x, \underset{˙}{1}⟩ = ⟨\underset{˙}{1}, \underset{˙}{1}⟩$
95	94	eceq1d	$⊢ x = \underset{˙}{1} \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
96		eqid	$⊢ [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim}$
97	64 2 3 4 6 7 96	rloc1r	$⊢ φ \to [⟨\underset{˙}{1}, \underset{˙}{1}⟩] \underset{˙}{\sim} = 1_{L}$
98	95 97	sylan9eqr	$⊢ (φ \land x = \underset{˙}{1}) \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = 1_{L}$
99		fvexd	$⊢ φ \to 1_{L} \in V$
100	5 98 52 99	fvmptd2	$⊢ φ \to F (\underset{˙}{1}) = 1_{L}$
101	33	ad2antrr	$⊢ ((φ \land a \in B) \land b \in B) \to R \in Ring$
102	52	ad2antrr	$⊢ ((φ \land a \in B) \land b \in B) \to \underset{˙}{1} \in B$
103	1 32 2 101 102	ringlidmd	$⊢ ((φ \land a \in B) \land b \in B) \to \underset{˙}{1} \cdot_{R} \underset{˙}{1} = \underset{˙}{1}$
104	103	eqcomd	$⊢ ((φ \land a \in B) \land b \in B) \to \underset{˙}{1} = \underset{˙}{1} \cdot_{R} \underset{˙}{1}$
105	104	opeq2d	$⊢ ((φ \land a \in B) \land b \in B) \to ⟨a \cdot_{R} b, \underset{˙}{1}⟩ = ⟨a \cdot_{R} b, \underset{˙}{1} \cdot_{R} \underset{˙}{1}⟩$
106	105	eceq1d	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a \cdot_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a \cdot_{R} b, \underset{˙}{1} \cdot_{R} \underset{˙}{1}⟩] \underset{˙}{\sim}$
107	6	ad2antrr	$⊢ ((φ \land a \in B) \land b \in B) \to R \in CRing$
108	7	ad2antrr	$⊢ ((φ \land a \in B) \land b \in B) \to S \in SubMnd ({mulGrp}_{R})$
109		simplr	$⊢ ((φ \land a \in B) \land b \in B) \to a \in B$
110		simpr	$⊢ ((φ \land a \in B) \land b \in B) \to b \in B$
111	108 12	syl	$⊢ ((φ \land a \in B) \land b \in B) \to \underset{˙}{1} \in S$
112	1 32 91 3 4 107 108 109 110 111 111 90	rlocmulval	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a \cdot_{R} b, \underset{˙}{1} \cdot_{R} \underset{˙}{1}⟩] \underset{˙}{\sim}$
113	106 112	eqtr4d	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a \cdot_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
114		opeq1	$⊢ x = a \cdot_{R} b \to ⟨x, \underset{˙}{1}⟩ = ⟨a \cdot_{R} b, \underset{˙}{1}⟩$
115	114	eceq1d	$⊢ x = a \cdot_{R} b \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a \cdot_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
116	1 32 101 109 110	ringcld	$⊢ ((φ \land a \in B) \land b \in B) \to a \cdot_{R} b \in B$
117		ecexg	$⊢ \underset{˙}{\sim} \in V \to [⟨a \cdot_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
118	16 117	mp1i	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a \cdot_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
119	5 115 116 118	fvmptd3	$⊢ ((φ \land a \in B) \land b \in B) \to F (a \cdot_{R} b) = [⟨a \cdot_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
120		opeq1	$⊢ x = a \to ⟨x, \underset{˙}{1}⟩ = ⟨a, \underset{˙}{1}⟩$
121	120	eceq1d	$⊢ x = a \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim}$
122		ecexg	$⊢ \underset{˙}{\sim} \in V \to [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
123	16 122	mp1i	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
124	5 121 109 123	fvmptd3	$⊢ ((φ \land a \in B) \land b \in B) \to F (a) = [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim}$
125		opeq1	$⊢ x = b \to ⟨x, \underset{˙}{1}⟩ = ⟨b, \underset{˙}{1}⟩$
126	125	eceq1d	$⊢ x = b \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
127		ecexg	$⊢ \underset{˙}{\sim} \in V \to [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
128	16 127	mp1i	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
129	5 126 110 128	fvmptd3	$⊢ ((φ \land a \in B) \land b \in B) \to F (b) = [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
130	124 129	oveq12d	$⊢ ((φ \land a \in B) \land b \in B) \to F (a) \cdot_{L} F (b) = [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} \cdot_{L} [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
131	113 119 130	3eqtr4d	$⊢ ((φ \land a \in B) \land b \in B) \to F (a \cdot_{R} b) = F (a) \cdot_{L} F (b)$
132	131	anasss	$⊢ (φ \land (a \in B \land b \in B)) \to F (a \cdot_{R} b) = F (a) \cdot_{L} F (b)$
133		eqid	$⊢ {Base}_{L} = {Base}_{L}$
134		eqid	$⊢ +_{L} = +_{L}$
135	18 5	fmptd	$⊢ φ \to F : B ⟶ (B \times S) / \underset{˙}{\sim}$
136	1 64 32 59 73 3 4 6 51	rlocbas	$⊢ φ \to (B \times S) / \underset{˙}{\sim} = {Base}_{L}$
137	136	feq3d	$⊢ φ \to (F : B ⟶ (B \times S) / \underset{˙}{\sim} \leftrightarrow F : B ⟶ {Base}_{L})$
138	135 137	mpbid	$⊢ φ \to F : B ⟶ {Base}_{L}$
139	1 32 2 101 109	ringridmd	$⊢ ((φ \land a \in B) \land b \in B) \to a \cdot_{R} \underset{˙}{1} = a$
140	1 32 2 101 110	ringridmd	$⊢ ((φ \land a \in B) \land b \in B) \to b \cdot_{R} \underset{˙}{1} = b$
141	139 140	oveq12d	$⊢ ((φ \land a \in B) \land b \in B) \to (a \cdot_{R} \underset{˙}{1}) +_{R} (b \cdot_{R} \underset{˙}{1}) = a +_{R} b$
142	141	eqcomd	$⊢ ((φ \land a \in B) \land b \in B) \to a +_{R} b = (a \cdot_{R} \underset{˙}{1}) +_{R} (b \cdot_{R} \underset{˙}{1})$
143	142 104	opeq12d	$⊢ ((φ \land a \in B) \land b \in B) \to ⟨a +_{R} b, \underset{˙}{1}⟩ = ⟨(a \cdot_{R} \underset{˙}{1}) +_{R} (b \cdot_{R} \underset{˙}{1}), \underset{˙}{1} \cdot_{R} \underset{˙}{1}⟩$
144	143	eceq1d	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a +_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨(a \cdot_{R} \underset{˙}{1}) +_{R} (b \cdot_{R} \underset{˙}{1}), \underset{˙}{1} \cdot_{R} \underset{˙}{1}⟩] \underset{˙}{\sim}$
145	1 32 91 3 4 107 108 109 110 111 111 134	rlocaddval	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} +_{L} [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨(a \cdot_{R} \underset{˙}{1}) +_{R} (b \cdot_{R} \underset{˙}{1}), \underset{˙}{1} \cdot_{R} \underset{˙}{1}⟩] \underset{˙}{\sim}$
146	144 145	eqtr4d	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a +_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} +_{L} [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
147		opeq1	$⊢ x = a +_{R} b \to ⟨x, \underset{˙}{1}⟩ = ⟨a +_{R} b, \underset{˙}{1}⟩$
148	147	eceq1d	$⊢ x = a +_{R} b \to [⟨x, \underset{˙}{1}⟩] \underset{˙}{\sim} = [⟨a +_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
149	20	ad2antrr	$⊢ ((φ \land a \in B) \land b \in B) \to R \in Grp$
150	1 91 149 109 110	grpcld	$⊢ ((φ \land a \in B) \land b \in B) \to a +_{R} b \in B$
151		ecexg	$⊢ \underset{˙}{\sim} \in V \to [⟨a +_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
152	16 151	mp1i	$⊢ ((φ \land a \in B) \land b \in B) \to [⟨a +_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim} \in V$
153	5 148 150 152	fvmptd3	$⊢ ((φ \land a \in B) \land b \in B) \to F (a +_{R} b) = [⟨a +_{R} b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
154	124 129	oveq12d	$⊢ ((φ \land a \in B) \land b \in B) \to F (a) +_{L} F (b) = [⟨a, \underset{˙}{1}⟩] \underset{˙}{\sim} +_{L} [⟨b, \underset{˙}{1}⟩] \underset{˙}{\sim}$
155	146 153 154	3eqtr4d	$⊢ ((φ \land a \in B) \land b \in B) \to F (a +_{R} b) = F (a) +_{L} F (b)$
156	155	anasss	$⊢ (φ \land (a \in B \land b \in B)) \to F (a +_{R} b) = F (a) +_{L} F (b)$
157	1 2 89 32 90 33 93 100 132 133 91 134 138 156	isrhmd	$⊢ φ \to F \in (R RingHom L)$
158	88 157	jca	$⊢ φ \to (F : B \underset{1-1}{⟶} (B \times S) / \underset{˙}{\sim} \land F \in (R RingHom L))$

Metamath Proof Explorer

Theorem rlocf1

Proof