erlval

Description: Value of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocval.1	$⊢ B = {Base}_{R}$
	rlocval.2	$⊢ \underset{˙}{0} = 0_{R}$
	rlocval.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rlocval.4	$⊢ \underset{˙}{-} = -_{R}$
	erlval.w	$⊢ W = B \times S$
	erlval.q	$⊢ \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
	erlval.20	$⊢ φ \to S \subseteq B$
Assertion	erlval	$⊢ φ \to R ~_{RL} S = \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		rlocval.1	$⊢ B = {Base}_{R}$
2		rlocval.2	$⊢ \underset{˙}{0} = 0_{R}$
3		rlocval.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		rlocval.4	$⊢ \underset{˙}{-} = -_{R}$
5		erlval.w	$⊢ W = B \times S$
6		erlval.q	$⊢ \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
7		erlval.20	$⊢ φ \to S \subseteq B$
8		simpr	$⊢ (φ \land R \in V) \to R \in V$
9	1	fvexi	$⊢ B \in V$
10	9	a1i	$⊢ (φ \land R \in V) \to B \in V$
11	7	adantr	$⊢ (φ \land R \in V) \to S \subseteq B$
12	10 11	ssexd	$⊢ (φ \land R \in V) \to S \in V$
13	10 12	xpexd	$⊢ (φ \land R \in V) \to B \times S \in V$
14	5 13	eqeltrid	$⊢ (φ \land R \in V) \to W \in V$
15	14 14	xpexd	$⊢ (φ \land R \in V) \to W \times W \in V$
16		simprll	$⊢ (φ \land ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})) \to a \in W$
17		simprlr	$⊢ (φ \land ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})) \to b \in W$
18	16 17	opabssxpd	$⊢ φ \to \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\} \subseteq W \times W$
19	18	adantr	$⊢ (φ \land R \in V) \to \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\} \subseteq W \times W$
20	15 19	ssexd	$⊢ (φ \land R \in V) \to \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\} \in V$
21	6 20	eqeltrid	$⊢ (φ \land R \in V) \to \underset{˙}{\sim} \in V$
22		fvexd	$⊢ (r = R \land s = S) \to \cdot_{r} \in V$
23		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
24	23	adantr	$⊢ (r = R \land s = S) \to \cdot_{r} = \cdot_{R}$
25	24 3	eqtr4di	$⊢ (r = R \land s = S) \to \cdot_{r} = \underset{˙}{\cdot}$
26		fvexd	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \in V$
27		vex	$⊢ s \in V$
28	27	a1i	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to s \in V$
29	26 28	xpexd	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \times s \in V$
30		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
31	30	ad2antrr	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} = {Base}_{R}$
32	31 1	eqtr4di	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} = B$
33		simplr	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to s = S$
34	32 33	xpeq12d	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \times s = B \times S$
35	34 5	eqtr4di	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to {Base}_{r} \times s = W$
36		simpr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to w = W$
37	36	eleq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (a \in w \leftrightarrow a \in W)$
38	36	eleq2d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (b \in w \leftrightarrow b \in W)$
39	37 38	anbi12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to ((a \in w \land b \in w) \leftrightarrow (a \in W \land b \in W))$
40	33	adantr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to s = S$
41		simplr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to x = \underset{˙}{\cdot}$
42		eqidd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to t = t$
43		fveq2	$⊢ r = R \to -_{r} = -_{R}$
44	43	ad3antrrr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to -_{r} = -_{R}$
45	44 4	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to -_{r} = \underset{˙}{-}$
46	41	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 1^{st} (a) x 2^{nd} (b) = 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)$
47	41	oveqd	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 1^{st} (b) x 2^{nd} (a) = 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)$
48	45 46 47	oveq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a)) = (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))$
49	41 42 48	oveq123d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)))$
50		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
51	50	ad3antrrr	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 0_{r} = 0_{R}$
52	51 2	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to 0_{r} = \underset{˙}{0}$
53	49 52	eqeq12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r} \leftrightarrow t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})$
54	40 53	rexeqbidv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (\exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})$
55	39 54	anbi12d	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to (((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r}) \leftrightarrow ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0}))$
56	55	opabbidv	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\} = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
57	56 6	eqtr4di	$⊢ (((r = R \land s = S) \land x = \underset{˙}{\cdot}) \land w = W) \to \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\} = \underset{˙}{\sim}$
58	29 35 57	csbied2	$⊢ ((r = R \land s = S) \land x = \underset{˙}{\cdot}) \to ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\} = \underset{˙}{\sim}$
59	22 25 58	csbied2	$⊢ (r = R \land s = S) \to ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\} = \underset{˙}{\sim}$
60		df-erl	$⊢ ~_{RL} = (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\})$
61	59 60	ovmpoga	$⊢ (R \in V \land S \in V \land \underset{˙}{\sim} \in V) \to R ~_{RL} S = \underset{˙}{\sim}$
62	8 12 21 61	syl3anc	$⊢ (φ \land R \in V) \to R ~_{RL} S = \underset{˙}{\sim}$
63	60	reldmmpo	$⊢ Rel dom ~_{RL}$
64	63	ovprc1	$⊢ \neg R \in V \to R ~_{RL} S = \emptyset$
65	64	adantl	$⊢ (φ \land \neg R \in V) \to R ~_{RL} S = \emptyset$
66	6 18	eqsstrid	$⊢ φ \to \underset{˙}{\sim} \subseteq W \times W$
67	66	adantr	$⊢ (φ \land \neg R \in V) \to \underset{˙}{\sim} \subseteq W \times W$
68		fvprc	$⊢ \neg R \in V \to {Base}_{R} = \emptyset$
69	1 68	eqtrid	$⊢ \neg R \in V \to B = \emptyset$
70	69	xpeq1d	$⊢ \neg R \in V \to B \times S = \emptyset \times S$
71		0xp	$⊢ \emptyset \times S = \emptyset$
72	70 71	eqtrdi	$⊢ \neg R \in V \to B \times S = \emptyset$
73	5 72	eqtrid	$⊢ \neg R \in V \to W = \emptyset$
74		id	$⊢ W = \emptyset \to W = \emptyset$
75	74 74	xpeq12d	$⊢ W = \emptyset \to W \times W = \emptyset \times \emptyset$
76		0xp	$⊢ \emptyset \times \emptyset = \emptyset$
77	75 76	eqtrdi	$⊢ W = \emptyset \to W \times W = \emptyset$
78	73 77	syl	$⊢ \neg R \in V \to W \times W = \emptyset$
79	78	adantl	$⊢ (φ \land \neg R \in V) \to W \times W = \emptyset$
80	67 79	sseqtrd	$⊢ (φ \land \neg R \in V) \to \underset{˙}{\sim} \subseteq \emptyset$
81		ss0	$⊢ \underset{˙}{\sim} \subseteq \emptyset \to \underset{˙}{\sim} = \emptyset$
82	80 81	syl	$⊢ (φ \land \neg R \in V) \to \underset{˙}{\sim} = \emptyset$
83	65 82	eqtr4d	$⊢ (φ \land \neg R \in V) \to R ~_{RL} S = \underset{˙}{\sim}$
84	62 83	pm2.61dan	$⊢ φ \to R ~_{RL} S = \underset{˙}{\sim}$

Metamath Proof Explorer

Theorem erlval

Proof