rlocisunit

Description: Characterize the units of the localization L of a ring R at S as the elements with a "numerator" P in the saturation T of S . (Contributed by Thierry Arnoux, 6-Jun-2026)

	Ref	Expression
Hypotheses	rlocisunit.b	$⊢ B = {Base}_{R}$
	rlocisunit.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rlocisunit.l	$⊢ L = R RLocal S$
	rlocisunit.w	$⊢ W = Unit (L)$
	rlocisunit.r	$⊢ φ \to R \in CRing$
	rlocisunit.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
	rlocisunit.e	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	rlocisunit.p	$⊢ φ \to P \in B$
	rlocisunit.q	$⊢ φ \to Q \in S$
	rlocisunit.t	$⊢ T = \{r \in B \| \exists s \in B r \underset{˙}{\cdot} s \in S\}$
Assertion	rlocisunit	$⊢ φ \to ([⟨P, Q⟩] \underset{˙}{\sim} \in W \leftrightarrow P \in T)$

Proof

Step	Hyp	Ref	Expression
1		rlocisunit.b	$⊢ B = {Base}_{R}$
2		rlocisunit.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rlocisunit.l	$⊢ L = R RLocal S$
4		rlocisunit.w	$⊢ W = Unit (L)$
5		rlocisunit.r	$⊢ φ \to R \in CRing$
6		rlocisunit.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
7		rlocisunit.e	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
8		rlocisunit.p	$⊢ φ \to P \in B$
9		rlocisunit.q	$⊢ φ \to Q \in S$
10		rlocisunit.t	$⊢ T = \{r \in B \| \exists s \in B r \underset{˙}{\cdot} s \in S\}$
11	10	eleq2i	$⊢ P \in T \leftrightarrow P \in \{r \in B \| \exists s \in B r \underset{˙}{\cdot} s \in S\}$
12		oveq1	$⊢ r = P \to r \underset{˙}{\cdot} s = P \underset{˙}{\cdot} s$
13	12	eleq1d	$⊢ r = P \to (r \underset{˙}{\cdot} s \in S \leftrightarrow P \underset{˙}{\cdot} s \in S)$
14	13	rexbidv	$⊢ r = P \to (\exists s \in B r \underset{˙}{\cdot} s \in S \leftrightarrow \exists s \in B P \underset{˙}{\cdot} s \in S)$
15	14	elrab	$⊢ P \in \{r \in B \| \exists s \in B r \underset{˙}{\cdot} s \in S\} \leftrightarrow (P \in B \land \exists s \in B P \underset{˙}{\cdot} s \in S)$
16	11 15	bitri	$⊢ P \in T \leftrightarrow (P \in B \land \exists s \in B P \underset{˙}{\cdot} s \in S)$
17	8	biantrurd	$⊢ φ \to (\exists s \in B P \underset{˙}{\cdot} s \in S \leftrightarrow (P \in B \land \exists s \in B P \underset{˙}{\cdot} s \in S))$
18	16 17	bitr4id	$⊢ φ \to (P \in T \leftrightarrow \exists s \in B P \underset{˙}{\cdot} s \in S)$
19		eqid	$⊢ {Base}_{L} = {Base}_{L}$
20		eqid	$⊢ \cdot_{L} = \cdot_{L}$
21		eqid	$⊢ 1_{L} = 1_{L}$
22		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
23		eqid	$⊢ 1_{R} = 1_{R}$
24	22 23	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
25	24	subm0cl	$⊢ S \in SubMnd ({mulGrp}_{R}) \to 1_{R} \in S$
26	6 25	syl	$⊢ φ \to 1_{R} \in S$
27	8 26	opelxpd	$⊢ φ \to ⟨P, 1_{R}⟩ \in (B \times S)$
28	7	ovexi	$⊢ \underset{˙}{\sim} \in V$
29	28	ecelqsi	$⊢ ⟨P, 1_{R}⟩ \in (B \times S) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
30	27 29	syl	$⊢ φ \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
31		eqid	$⊢ 0_{R} = 0_{R}$
32		eqid	$⊢ -_{R} = -_{R}$
33		eqid	$⊢ B \times S = B \times S$
34	22 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
35	34	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq B$
36	6 35	syl	$⊢ φ \to S \subseteq B$
37	1 31 2 32 33 3 7 5 36	rlocbas	$⊢ φ \to (B \times S) / \underset{˙}{\sim} = {Base}_{L}$
38	30 37	eleqtrd	$⊢ φ \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \in {Base}_{L}$
39		eqid	$⊢ +_{R} = +_{R}$
40	1 2 39 3 7 5 6	rloccring	$⊢ φ \to L \in CRing$
41	19 4 20 21 38 40	isunitc	$⊢ φ \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \leftrightarrow \exists x \in {Base}_{L} [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L})$
42	5	crngringd	$⊢ φ \to R \in Ring$
43	42	ad7antr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to R \in Ring$
44	36	ad7antr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to S \subseteq B$
45		simplr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \in S$
46	44 45	sseldd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \in B$
47		simpllr	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to r \in B$
48	47	ad2antrr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to r \in B$
49	1 2 43 46 48	ringcld	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \underset{˙}{\cdot} r \in B$
50		oveq2	$⊢ u = t \underset{˙}{\cdot} r \to P \underset{˙}{\cdot} u = P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r)$
51	50	eleq1d	$⊢ u = t \underset{˙}{\cdot} r \to (P \underset{˙}{\cdot} u \in S \leftrightarrow P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r) \in S)$
52	51	adantl	$⊢ ((((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \land u = t \underset{˙}{\cdot} r) \to (P \underset{˙}{\cdot} u \in S \leftrightarrow P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r) \in S)$
53	5	ad7antr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to R \in CRing$
54	8	ad7antr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to P \in B$
55	1 2 53 54 46 48	crng12d	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r) = t \underset{˙}{\cdot} (P \underset{˙}{\cdot} r)$
56	1 2 43 54 48	ringcld	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to P \underset{˙}{\cdot} r \in B$
57	1 2 23 43 56	ringridmd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to (P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R} = P \underset{˙}{\cdot} r$
58	57	oveq2d	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (P \underset{˙}{\cdot} r)$
59	55 58	eqtr4d	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r) = t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R})$
60		simpr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))$
61	36 26	sseldd	$⊢ φ \to 1_{R} \in B$
62	61	ad7antr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to 1_{R} \in B$
63		simplr	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to s \in S$
64	63	ad2antrr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to s \in S$
65	44 64	sseldd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to s \in B$
66	1 2 43 62 65	ringcld	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to 1_{R} \underset{˙}{\cdot} s \in B$
67	1 2 23 43 66	ringlidmd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to 1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s) = 1_{R} \underset{˙}{\cdot} s$
68	1 2 23 43 65	ringlidmd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to 1_{R} \underset{˙}{\cdot} s = s$
69	67 68	eqtrd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to 1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s) = s$
70	69	oveq2d	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s)) = t \underset{˙}{\cdot} s$
71	59 60 70	3eqtrd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r) = t \underset{˙}{\cdot} s$
72	22 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
73	6	ad7antr	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to S \in SubMnd ({mulGrp}_{R})$
74	72 73 45 64	submcld	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to t \underset{˙}{\cdot} s \in S$
75	71 74	eqeltrd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to P \underset{˙}{\cdot} (t \underset{˙}{\cdot} r) \in S$
76	49 52 75	rspcedvd	$⊢ (((((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \land t \in S) \land t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))) \to \exists u \in B P \underset{˙}{\cdot} u \in S$
77		simp-5l	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to φ$
78		simpr	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to x = [⟨r, s⟩] \underset{˙}{\sim}$
79	78	oveq2d	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨r, s⟩] \underset{˙}{\sim}$
80		simp-4r	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}$
81	5	ad2antrr	$⊢ ((φ \land r \in B) \land s \in S) \to R \in CRing$
82	6	ad2antrr	$⊢ ((φ \land r \in B) \land s \in S) \to S \in SubMnd ({mulGrp}_{R})$
83	8	ad2antrr	$⊢ ((φ \land r \in B) \land s \in S) \to P \in B$
84		simplr	$⊢ ((φ \land r \in B) \land s \in S) \to r \in B$
85	82 25	syl	$⊢ ((φ \land r \in B) \land s \in S) \to 1_{R} \in S$
86		simpr	$⊢ ((φ \land r \in B) \land s \in S) \to s \in S$
87	1 2 39 3 7 81 82 83 84 85 86 20	rlocmulval	$⊢ ((φ \land r \in B) \land s \in S) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨r, s⟩] \underset{˙}{\sim} = [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim}$
88	77 47 63 87	syl21anc	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨r, s⟩] \underset{˙}{\sim} = [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim}$
89	79 80 88	3eqtr3rd	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = 1_{L}$
90		eqid	$⊢ [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}$
91	31 23 3 7 5 6 90	rloc1r	$⊢ φ \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = 1_{L}$
92	91	ad5antr	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = 1_{L}$
93	89 92	eqtr4d	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}$
94	81	adantr	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to R \in CRing$
95	82	adantr	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to S \in SubMnd ({mulGrp}_{R})$
96	42	ad2antrr	$⊢ ((φ \land r \in B) \land s \in S) \to R \in Ring$
97	1 2 96 83 84	ringcld	$⊢ ((φ \land r \in B) \land s \in S) \to P \underset{˙}{\cdot} r \in B$
98	97	adantr	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to P \underset{˙}{\cdot} r \in B$
99	72 82 85 86	submcld	$⊢ ((φ \land r \in B) \land s \in S) \to 1_{R} \underset{˙}{\cdot} s \in S$
100	99	adantr	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to 1_{R} \underset{˙}{\cdot} s \in S$
101	61	ad3antrrr	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to 1_{R} \in B$
102	95 25	syl	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to 1_{R} \in S$
103		simpr	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}$
104	1 7 2 94 95 98 100 101 102 103	erld2	$⊢ (((φ \land r \in B) \land s \in S) \land [⟨P \underset{˙}{\cdot} r, 1_{R} \underset{˙}{\cdot} s⟩] \underset{˙}{\sim} = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}) \to \exists t \in S t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))$
105	77 47 63 93 104	syl1111anc	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to \exists t \in S t \underset{˙}{\cdot} ((P \underset{˙}{\cdot} r) \underset{˙}{\cdot} 1_{R}) = t \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} (1_{R} \underset{˙}{\cdot} s))$
106	76 105	r19.29a	$⊢ (((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land s \in S) \land x = [⟨r, s⟩] \underset{˙}{\sim}) \to \exists u \in B P \underset{˙}{\cdot} u \in S$
107	106	r19.29an	$⊢ ((((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \land r \in B) \land \exists s \in S x = [⟨r, s⟩] \underset{˙}{\sim}) \to \exists u \in B P \underset{˙}{\cdot} u \in S$
108	37	eleq2d	$⊢ φ \to (x \in ((B \times S) / \underset{˙}{\sim}) \leftrightarrow x \in {Base}_{L})$
109	108	biimpar	$⊢ (φ \land x \in {Base}_{L}) \to x \in ((B \times S) / \underset{˙}{\sim})$
110	109	adantr	$⊢ ((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \to x \in ((B \times S) / \underset{˙}{\sim})$
111	110	elrlocbasi	$⊢ ((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \to \exists r \in B \exists s \in S x = [⟨r, s⟩] \underset{˙}{\sim}$
112	107 111	r19.29a	$⊢ ((φ \land x \in {Base}_{L}) \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \to \exists u \in B P \underset{˙}{\cdot} u \in S$
113	112	r19.29an	$⊢ (φ \land \exists x \in {Base}_{L} [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}) \to \exists u \in B P \underset{˙}{\cdot} u \in S$
114		simplr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to u \in B$
115		simpr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to P \underset{˙}{\cdot} u \in S$
116	114 115	opelxpd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to ⟨u, P \underset{˙}{\cdot} u⟩ \in (B \times S)$
117	28	ecelqsi	$⊢ ⟨u, P \underset{˙}{\cdot} u⟩ \in (B \times S) \to [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
118	116 117	syl	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
119	37	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to (B \times S) / \underset{˙}{\sim} = {Base}_{L}$
120	118 119	eleqtrd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} \in {Base}_{L}$
121		oveq2	$⊢ x = [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim}$
122	121	eqeq1d	$⊢ x = [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L} \leftrightarrow [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} = 1_{L})$
123	122	adantl	$⊢ (((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \land x = [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim}) \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L} \leftrightarrow [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} = 1_{L})$
124	5	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to R \in CRing$
125	6	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to S \in SubMnd ({mulGrp}_{R})$
126	8	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to P \in B$
127	125 25	syl	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to 1_{R} \in S$
128	1 2 39 3 7 124 125 126 114 127 115 20	rlocmulval	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} = [⟨P \underset{˙}{\cdot} u, 1_{R} \underset{˙}{\cdot} (P \underset{˙}{\cdot} u)⟩] \underset{˙}{\sim}$
129	1 31 23 2 32 33 7 5 6	erler	$⊢ φ \to \underset{˙}{\sim} Er (B \times S)$
130	129	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to \underset{˙}{\sim} Er (B \times S)$
131		eqidd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to ⟨1_{R}, 1_{R}⟩ = ⟨1_{R}, 1_{R}⟩$
132		eqidd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to P \underset{˙}{\cdot} u = P \underset{˙}{\cdot} u$
133	42	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to R \in Ring$
134	1 2 133 126 114	ringcld	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to P \underset{˙}{\cdot} u \in B$
135	1 2 23 133 134	ringlidmd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to 1_{R} \underset{˙}{\cdot} (P \underset{˙}{\cdot} u) = P \underset{˙}{\cdot} u$
136	132 135	opeq12d	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to ⟨P \underset{˙}{\cdot} u, 1_{R} \underset{˙}{\cdot} (P \underset{˙}{\cdot} u)⟩ = ⟨P \underset{˙}{\cdot} u, P \underset{˙}{\cdot} u⟩$
137	61	ad2antrr	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to 1_{R} \in B$
138	1 2 23 133 134	ringridmd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to (P \underset{˙}{\cdot} u) \underset{˙}{\cdot} 1_{R} = P \underset{˙}{\cdot} u$
139	138	eqcomd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to P \underset{˙}{\cdot} u = (P \underset{˙}{\cdot} u) \underset{˙}{\cdot} 1_{R}$
140	1 7 124 125 2 131 136 137 134 127 115 115 139 139	erlbr2d	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to ⟨1_{R}, 1_{R}⟩ \underset{˙}{\sim} ⟨P \underset{˙}{\cdot} u, 1_{R} \underset{˙}{\cdot} (P \underset{˙}{\cdot} u)⟩$
141	130 140	erthi	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨P \underset{˙}{\cdot} u, 1_{R} \underset{˙}{\cdot} (P \underset{˙}{\cdot} u)⟩] \underset{˙}{\sim}$
142	31 23 3 7 124 125 90	rloc1r	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = 1_{L}$
143	128 141 142	3eqtr2d	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨u, P \underset{˙}{\cdot} u⟩] \underset{˙}{\sim} = 1_{L}$
144	120 123 143	rspcedvd	$⊢ ((φ \land u \in B) \land P \underset{˙}{\cdot} u \in S) \to \exists x \in {Base}_{L} [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}$
145	144	r19.29an	$⊢ (φ \land \exists u \in B P \underset{˙}{\cdot} u \in S) \to \exists x \in {Base}_{L} [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L}$
146	113 145	impbida	$⊢ φ \to (\exists x \in {Base}_{L} [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = 1_{L} \leftrightarrow \exists u \in B P \underset{˙}{\cdot} u \in S)$
147		oveq2	$⊢ u = s \to P \underset{˙}{\cdot} u = P \underset{˙}{\cdot} s$
148	147	eleq1d	$⊢ u = s \to (P \underset{˙}{\cdot} u \in S \leftrightarrow P \underset{˙}{\cdot} s \in S)$
149	148	cbvrexvw	$⊢ \exists u \in B P \underset{˙}{\cdot} u \in S \leftrightarrow \exists s \in B P \underset{˙}{\cdot} s \in S$
150	149	a1i	$⊢ φ \to (\exists u \in B P \underset{˙}{\cdot} u \in S \leftrightarrow \exists s \in B P \underset{˙}{\cdot} s \in S)$
151	41 146 150	3bitrd	$⊢ φ \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \leftrightarrow \exists s \in B P \underset{˙}{\cdot} s \in S)$
152	5	adantr	$⊢ (φ \land Q \in S) \to R \in CRing$
153	6	adantr	$⊢ (φ \land Q \in S) \to S \in SubMnd ({mulGrp}_{R})$
154		simpr	$⊢ (φ \land Q \in S) \to Q \in S$
155	1 23 7 3 4 152 153 154	rlocinvunit	$⊢ (φ \land Q \in S) \to [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W$
156	9 155	mpdan	$⊢ φ \to [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W$
157	156	biantrud	$⊢ φ \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \leftrightarrow ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \land [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W))$
158	1 2 39 3 7 5 6 8 61 26 9 20	rlocmulval	$⊢ φ \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, Q⟩] \underset{˙}{\sim} = [⟨P \underset{˙}{\cdot} 1_{R}, 1_{R} \underset{˙}{\cdot} Q⟩] \underset{˙}{\sim}$
159	1 2 23 42 8	ringridmd	$⊢ φ \to P \underset{˙}{\cdot} 1_{R} = P$
160	36 9	sseldd	$⊢ φ \to Q \in B$
161	1 2 23 42 160	ringlidmd	$⊢ φ \to 1_{R} \underset{˙}{\cdot} Q = Q$
162	159 161	opeq12d	$⊢ φ \to ⟨P \underset{˙}{\cdot} 1_{R}, 1_{R} \underset{˙}{\cdot} Q⟩ = ⟨P, Q⟩$
163	162	eceq1d	$⊢ φ \to [⟨P \underset{˙}{\cdot} 1_{R}, 1_{R} \underset{˙}{\cdot} Q⟩] \underset{˙}{\sim} = [⟨P, Q⟩] \underset{˙}{\sim}$
164	158 163	eqtrd	$⊢ φ \to [⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, Q⟩] \underset{˙}{\sim} = [⟨P, Q⟩] \underset{˙}{\sim}$
165	164	eleq1d	$⊢ φ \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W \leftrightarrow [⟨P, Q⟩] \underset{˙}{\sim} \in W)$
166	61 9	opelxpd	$⊢ φ \to ⟨1_{R}, Q⟩ \in (B \times S)$
167	28	ecelqsi	$⊢ ⟨1_{R}, Q⟩ \in (B \times S) \to [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
168	166 167	syl	$⊢ φ \to [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
169	168 37	eleqtrd	$⊢ φ \to [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in {Base}_{L}$
170	4 20 19	unitmulclb	$⊢ (L \in CRing \land [⟨P, 1_{R}⟩] \underset{˙}{\sim} \in {Base}_{L} \land [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in {Base}_{L}) \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W \leftrightarrow ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \land [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W))$
171	40 38 169 170	syl3anc	$⊢ φ \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W \leftrightarrow ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \land [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W))$
172	165 171	bitr3d	$⊢ φ \to ([⟨P, Q⟩] \underset{˙}{\sim} \in W \leftrightarrow ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \land [⟨1_{R}, Q⟩] \underset{˙}{\sim} \in W))$
173	157 172	bitr4d	$⊢ φ \to ([⟨P, 1_{R}⟩] \underset{˙}{\sim} \in W \leftrightarrow [⟨P, Q⟩] \underset{˙}{\sim} \in W)$
174	18 151 173	3bitr2rd	$⊢ φ \to ([⟨P, Q⟩] \underset{˙}{\sim} \in W \leftrightarrow P \in T)$

Metamath Proof Explorer

Theorem rlocisunit

Proof