fracerl

Description: Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025)

	Ref	Expression
Hypotheses	fracerl.1	$⊢ B = {Base}_{R}$
	fracerl.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	fracerl.3	No typesetting found for \|- .~ = ( R ~RL ( RLReg ` R ) ) with typecode \|-
	fracerl.4	$⊢ φ \to R \in CRing$
	fracerl.5	$⊢ φ \to E \in B$
	fracerl.6	$⊢ φ \to G \in B$
	fracerl.7	$⊢ φ \to F \in RLReg (R)$
	fracerl.8	$⊢ φ \to H \in RLReg (R)$
Assertion	fracerl	$⊢ φ \to (⟨E, F⟩ \underset{˙}{\sim} ⟨G, H⟩ \leftrightarrow E \underset{˙}{\cdot} H = G \underset{˙}{\cdot} F)$

Proof

Step	Hyp	Ref	Expression
1		fracerl.1	$⊢ B = {Base}_{R}$
2		fracerl.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		fracerl.3	Could not format .~ = ( R ~RL ( RLReg ` R ) ) : No typesetting found for \|- .~ = ( R ~RL ( RLReg ` R ) ) with typecode \|-
4		fracerl.4	$⊢ φ \to R \in CRing$
5		fracerl.5	$⊢ φ \to E \in B$
6		fracerl.6	$⊢ φ \to G \in B$
7		fracerl.7	$⊢ φ \to F \in RLReg (R)$
8		fracerl.8	$⊢ φ \to H \in RLReg (R)$
9		eqid	$⊢ 0_{R} = 0_{R}$
10		eqid	$⊢ -_{R} = -_{R}$
11		eqid	$⊢ B \times RLReg (R) = B \times RLReg (R)$
12		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (B \times RLReg (R)) \land b \in (B \times RLReg (R))) \land \exists t \in RLReg (R) t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = 0_{R})\} = \{⟨a, b⟩ \| ((a \in (B \times RLReg (R)) \land b \in (B \times RLReg (R))) \land \exists t \in RLReg (R) t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = 0_{R})\}$
13		eqid	$⊢ RLReg (R) = RLReg (R)$
14	13 1	rrgss	$⊢ RLReg (R) \subseteq B$
15	14	a1i	$⊢ φ \to RLReg (R) \subseteq B$
16	1 9 2 10 11 12 15	erlval	Could not format ( ph -> ( R ~RL ( RLReg ` R ) ) = { <. a , b >. \| ( ( a e. ( B X. ( RLReg ` R ) ) /\ b e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } ) : No typesetting found for \|- ( ph -> ( R ~RL ( RLReg ` R ) ) = { <. a , b >. \| ( ( a e. ( B X. ( RLReg ` R ) ) /\ b e. ( B X. ( RLReg ` R ) ) ) /\ E. t e. ( RLReg ` R ) ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( -g ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( 0g ` R ) ) } ) with typecode \|-
17	3 16	eqtrid	$⊢ φ \to \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in (B \times RLReg (R)) \land b \in (B \times RLReg (R))) \land \exists t \in RLReg (R) t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = 0_{R})\}$
18		simprl	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to a = ⟨E, F⟩$
19	18	fveq2d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (a) = 1^{st} (⟨E, F⟩)$
20	7	adantr	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to F \in RLReg (R)$
21		op1stg	$⊢ (E \in B \land F \in RLReg (R)) \to 1^{st} (⟨E, F⟩) = E$
22	5 20 21	syl2an2r	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (⟨E, F⟩) = E$
23	19 22	eqtrd	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (a) = E$
24		simprr	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to b = ⟨G, H⟩$
25	24	fveq2d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 2^{nd} (b) = 2^{nd} (⟨G, H⟩)$
26	8	adantr	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to H \in RLReg (R)$
27		op2ndg	$⊢ (G \in B \land H \in RLReg (R)) \to 2^{nd} (⟨G, H⟩) = H$
28	6 26 27	syl2an2r	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 2^{nd} (⟨G, H⟩) = H$
29	25 28	eqtrd	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 2^{nd} (b) = H$
30	23 29	oveq12d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b) = E \underset{˙}{\cdot} H$
31	24	fveq2d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (b) = 1^{st} (⟨G, H⟩)$
32		op1stg	$⊢ (G \in B \land H \in RLReg (R)) \to 1^{st} (⟨G, H⟩) = G$
33	6 26 32	syl2an2r	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (⟨G, H⟩) = G$
34	31 33	eqtrd	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (b) = G$
35	18	fveq2d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 2^{nd} (a) = 2^{nd} (⟨E, F⟩)$
36		op2ndg	$⊢ (E \in B \land F \in RLReg (R)) \to 2^{nd} (⟨E, F⟩) = F$
37	5 20 36	syl2an2r	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 2^{nd} (⟨E, F⟩) = F$
38	35 37	eqtrd	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 2^{nd} (a) = F$
39	34 38	oveq12d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a) = G \underset{˙}{\cdot} F$
40	30 39	oveq12d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)) = (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)$
41	40	oveq2d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F))$
42	41	eqeq1d	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to (t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = 0_{R} \leftrightarrow t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R})$
43	42	rexbidv	$⊢ (φ \land (a = ⟨E, F⟩ \land b = ⟨G, H⟩)) \to (\exists t \in RLReg (R) t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) -_{R} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = 0_{R} \leftrightarrow \exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R})$
44	17 43	brab2d	$⊢ φ \to (⟨E, F⟩ \underset{˙}{\sim} ⟨G, H⟩ \leftrightarrow ((⟨E, F⟩ \in (B \times RLReg (R)) \land ⟨G, H⟩ \in (B \times RLReg (R))) \land \exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}))$
45	5 7	opelxpd	$⊢ φ \to ⟨E, F⟩ \in (B \times RLReg (R))$
46	6 8	opelxpd	$⊢ φ \to ⟨G, H⟩ \in (B \times RLReg (R))$
47	45 46	jca	$⊢ φ \to (⟨E, F⟩ \in (B \times RLReg (R)) \land ⟨G, H⟩ \in (B \times RLReg (R)))$
48	47	biantrurd	$⊢ φ \to (\exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R} \leftrightarrow ((⟨E, F⟩ \in (B \times RLReg (R)) \land ⟨G, H⟩ \in (B \times RLReg (R))) \land \exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}))$
49		simplr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to t \in RLReg (R)$
50	4	crnggrpd	$⊢ φ \to R \in Grp$
51	50	ad2antrr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to R \in Grp$
52	4	crngringd	$⊢ φ \to R \in Ring$
53	52	ad2antrr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to R \in Ring$
54	5	ad2antrr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to E \in B$
55	14 8	sselid	$⊢ φ \to H \in B$
56	55	ad2antrr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to H \in B$
57	1 2 53 54 56	ringcld	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to E \underset{˙}{\cdot} H \in B$
58	6	ad2antrr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to G \in B$
59	14 7	sselid	$⊢ φ \to F \in B$
60	59	ad2antrr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to F \in B$
61	1 2 53 58 60	ringcld	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to G \underset{˙}{\cdot} F \in B$
62	1 10	grpsubcl	$⊢ (R \in Grp \land E \underset{˙}{\cdot} H \in B \land G \underset{˙}{\cdot} F \in B) \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) \in B$
63	51 57 61 62	syl3anc	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) \in B$
64		simpr	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}$
65	13 1 2 9	rrgeq0i	$⊢ (t \in RLReg (R) \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) \in B) \to (t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R} \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R})$
66	65	imp	$⊢ ((t \in RLReg (R) \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) \in B) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}$
67	49 63 64 66	syl21anc	$⊢ ((φ \land t \in RLReg (R)) \land t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}$
68	67	r19.29an	$⊢ (φ \land \exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}) \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}$
69		oveq1	$⊢ t = 1_{R} \to t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 1_{R} \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F))$
70	69	eqeq1d	$⊢ t = 1_{R} \to (t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R} \leftrightarrow 1_{R} \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R})$
71		eqid	$⊢ 1_{R} = 1_{R}$
72	71 13 52	1rrg	$⊢ φ \to 1_{R} \in RLReg (R)$
73	72	adantr	$⊢ (φ \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}) \to 1_{R} \in RLReg (R)$
74		simpr	$⊢ (φ \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}) \to (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}$
75	74	oveq2d	$⊢ (φ \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}) \to 1_{R} \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 1_{R} \underset{˙}{\cdot} 0_{R}$
76	1 71	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
77	52 76	syl	$⊢ φ \to 1_{R} \in B$
78	1 2 9 52 77	ringrzd	$⊢ φ \to 1_{R} \underset{˙}{\cdot} 0_{R} = 0_{R}$
79	78	adantr	$⊢ (φ \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}) \to 1_{R} \underset{˙}{\cdot} 0_{R} = 0_{R}$
80	75 79	eqtrd	$⊢ (φ \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}) \to 1_{R} \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}$
81	70 73 80	rspcedvdw	$⊢ (φ \land (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R}) \to \exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R}$
82	68 81	impbida	$⊢ φ \to (\exists t \in RLReg (R) t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F)) = 0_{R} \leftrightarrow (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R})$
83	44 48 82	3bitr2d	$⊢ φ \to (⟨E, F⟩ \underset{˙}{\sim} ⟨G, H⟩ \leftrightarrow (E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R})$
84	1 2 52 5 55	ringcld	$⊢ φ \to E \underset{˙}{\cdot} H \in B$
85	1 2 52 6 59	ringcld	$⊢ φ \to G \underset{˙}{\cdot} F \in B$
86	1 9 10	grpsubeq0	$⊢ (R \in Grp \land E \underset{˙}{\cdot} H \in B \land G \underset{˙}{\cdot} F \in B) \to ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R} \leftrightarrow E \underset{˙}{\cdot} H = G \underset{˙}{\cdot} F)$
87	50 84 85 86	syl3anc	$⊢ φ \to ((E \underset{˙}{\cdot} H) -_{R} (G \underset{˙}{\cdot} F) = 0_{R} \leftrightarrow E \underset{˙}{\cdot} H = G \underset{˙}{\cdot} F)$
88	83 87	bitrd	$⊢ φ \to (⟨E, F⟩ \underset{˙}{\sim} ⟨G, H⟩ \leftrightarrow E \underset{˙}{\cdot} H = G \underset{˙}{\cdot} F)$

Metamath Proof Explorer

Theorem fracerl

Proof