rloccring

Description: The ring localization L of a commutative ring R by a multiplicatively closed set S is itself a commutative ring. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocaddval.1	$⊢ B = {Base}_{R}$
	rlocaddval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rlocaddval.3	$⊢ \underset{˙}{+} = +_{R}$
	rlocaddval.4	No typesetting found for \|- L = ( R RLocal S ) with typecode \|-
	rlocaddval.5	No typesetting found for \|- .~ = ( R ~RL S ) with typecode \|-
	rlocaddval.r	$⊢ φ \to R \in CRing$
	rlocaddval.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
Assertion	rloccring	$⊢ φ \to L \in CRing$

Proof

Step	Hyp	Ref	Expression
1		rlocaddval.1	$⊢ B = {Base}_{R}$
2		rlocaddval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rlocaddval.3	$⊢ \underset{˙}{+} = +_{R}$
4		rlocaddval.4	Could not format L = ( R RLocal S ) : No typesetting found for \|- L = ( R RLocal S ) with typecode \|-
5		rlocaddval.5	Could not format .~ = ( R ~RL S ) : No typesetting found for \|- .~ = ( R ~RL S ) with typecode \|-
6		rlocaddval.r	$⊢ φ \to R \in CRing$
7		rlocaddval.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
8		eqid	$⊢ 0_{R} = 0_{R}$
9		eqid	$⊢ -_{R} = -_{R}$
10		eqid	$⊢ B \times S = B \times S$
11		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
12	11 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
13	12	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq B$
14	7 13	syl	$⊢ φ \to S \subseteq B$
15	1 8 2 9 10 4 5 6 14	rlocbas	$⊢ φ \to (B \times S) / \underset{˙}{\sim} = {Base}_{L}$
16		eqidd	$⊢ φ \to +_{L} = +_{L}$
17		eqidd	$⊢ φ \to \cdot_{L} = \cdot_{L}$
18		eqid	$⊢ {Base}_{L} = {Base}_{L}$
19		eqid	$⊢ 0_{L} = 0_{L}$
20		eqid	$⊢ +_{L} = +_{L}$
21	6	crngringd	$⊢ φ \to R \in Ring$
22	1 8	ring0cl	$⊢ R \in Ring \to 0_{R} \in B$
23	21 22	syl	$⊢ φ \to 0_{R} \in B$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	11 24	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
26	25	subm0cl	$⊢ S \in SubMnd ({mulGrp}_{R}) \to 1_{R} \in S$
27	7 26	syl	$⊢ φ \to 1_{R} \in S$
28	23 27	opelxpd	$⊢ φ \to ⟨0_{R}, 1_{R}⟩ \in (B \times S)$
29	5	ovexi	$⊢ \underset{˙}{\sim} \in V$
30	29	ecelqsi	$⊢ ⟨0_{R}, 1_{R}⟩ \in (B \times S) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
31	28 30	syl	$⊢ φ \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
32	31 15	eleqtrd	$⊢ φ \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} \in {Base}_{L}$
33	15	eleq2d	$⊢ φ \to (x \in ((B \times S) / \underset{˙}{\sim}) \leftrightarrow x \in {Base}_{L})$
34	33	biimpar	$⊢ (φ \land x \in {Base}_{L}) \to x \in ((B \times S) / \underset{˙}{\sim})$
35		simpr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x = [⟨a, b⟩] \underset{˙}{\sim}$
36	35	oveq2d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} x = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim}$
37	21	ad4antr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to R \in Ring$
38	7	ad4antr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to S \in SubMnd ({mulGrp}_{R})$
39	38 13	syl	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to S \subseteq B$
40		simplr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \in S$
41	39 40	sseldd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \in B$
42	1 2 8 37 41	ringlzd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 0_{R} \underset{˙}{\cdot} b = 0_{R}$
43		simpllr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a \in B$
44	1 2 24 37 43	ringridmd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} 1_{R} = a$
45	42 44	oveq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (0_{R} \underset{˙}{\cdot} b) +_{R} (a \underset{˙}{\cdot} 1_{R}) = 0_{R} +_{R} a$
46		eqid	$⊢ +_{R} = +_{R}$
47	37	ringgrpd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to R \in Grp$
48	1 46 8 47 43	grplidd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 0_{R} +_{R} a = a$
49	45 48	eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (0_{R} \underset{˙}{\cdot} b) +_{R} (a \underset{˙}{\cdot} 1_{R}) = a$
50	1 2 24 37 41	ringlidmd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 1_{R} \underset{˙}{\cdot} b = b$
51	49 50	opeq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨(0_{R} \underset{˙}{\cdot} b) +_{R} (a \underset{˙}{\cdot} 1_{R}), 1_{R} \underset{˙}{\cdot} b⟩ = ⟨a, b⟩$
52	51	eceq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨(0_{R} \underset{˙}{\cdot} b) +_{R} (a \underset{˙}{\cdot} 1_{R}), 1_{R} \underset{˙}{\cdot} b⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
53	6	ad4antr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to R \in CRing$
54	23	ad4antr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 0_{R} \in B$
55	38 26	syl	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 1_{R} \in S$
56	1 2 46 4 5 53 38 54 43 55 40 20	rlocaddval	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨(0_{R} \underset{˙}{\cdot} b) +_{R} (a \underset{˙}{\cdot} 1_{R}), 1_{R} \underset{˙}{\cdot} b⟩] \underset{˙}{\sim}$
57	52 56 35	3eqtr4d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim} = x$
58	36 57	eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} x = x$
59		simpr	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to x \in ((B \times S) / \underset{˙}{\sim})$
60	59	elrlocbasi	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to \exists a \in B \exists b \in S x = [⟨a, b⟩] \underset{˙}{\sim}$
61	58 60	r19.29vva	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} x = x$
62	34 61	syldan	$⊢ (φ \land x \in {Base}_{L}) \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} +_{L} x = x$
63	1 2 3 4 5 53 38 43 54 40 55 20	rlocaddval	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (0_{R} \underset{˙}{\cdot} b), b \underset{˙}{\cdot} 1_{R}⟩] \underset{˙}{\sim}$
64	35	oveq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x +_{L} [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim}$
65	44 42	oveq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (0_{R} \underset{˙}{\cdot} b) = a \underset{˙}{+} 0_{R}$
66	1 3 8 47 43	grpridd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a \underset{˙}{+} 0_{R} = a$
67	65 66	eqtr2d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a = (a \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (0_{R} \underset{˙}{\cdot} b)$
68	1 2 24 37 41	ringridmd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} 1_{R} = b$
69	68	eqcomd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b = b \underset{˙}{\cdot} 1_{R}$
70	67 69	opeq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨a, b⟩ = ⟨(a \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (0_{R} \underset{˙}{\cdot} b), b \underset{˙}{\cdot} 1_{R}⟩$
71	70	eceq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (0_{R} \underset{˙}{\cdot} b), b \underset{˙}{\cdot} 1_{R}⟩] \underset{˙}{\sim}$
72	35 71	eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x = [⟨(a \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (0_{R} \underset{˙}{\cdot} b), b \underset{˙}{\cdot} 1_{R}⟩] \underset{˙}{\sim}$
73	63 64 72	3eqtr4d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x +_{L} [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} = x$
74	73 60	r19.29vva	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to x +_{L} [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} = x$
75	34 74	syldan	$⊢ (φ \land x \in {Base}_{L}) \to x +_{L} [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} = x$
76	18 19 20 32 62 75	ismgmid2	$⊢ φ \to [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} = 0_{L}$
77		simp-4r	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x = [⟨a, b⟩] \underset{˙}{\sim}$
78		simpr	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to y = [⟨c, d⟩] \underset{˙}{\sim}$
79	77 78	oveq12d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x +_{L} y = [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}$
80	6	ad8antr	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to R \in CRing$
81	7	ad8antr	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to S \in SubMnd ({mulGrp}_{R})$
82		simp-6r	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to a \in B$
83		simpllr	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to c \in B$
84		simp-5r	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to b \in S$
85		simplr	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to d \in S$
86	1 2 3 4 5 80 81 82 83 84 85 20	rlocaddval	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim}$
87	80	crnggrpd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to R \in Grp$
88	21	ad8antr	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to R \in Ring$
89	81 13	syl	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to S \subseteq B$
90	89 85	sseldd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to d \in B$
91	1 2 88 82 90	ringcld	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} d \in B$
92	89 84	sseldd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to b \in B$
93	1 2 88 83 92	ringcld	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to c \underset{˙}{\cdot} b \in B$
94	1 3 87 91 93	grpcld	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b) \in B$
95	11 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
96	95 81 84 85	submcld	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} d \in S$
97	94 96	opelxpd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to ⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩ \in (B \times S)$
98	29	ecelqsi	$⊢ ⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩ \in (B \times S) \to [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
99	97 98	syl	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
100	86 99	eqeltrd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
101	79 100	eqeltrd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x +_{L} y \in ((B \times S) / \underset{˙}{\sim})$
102		simp-4r	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to y \in ((B \times S) / \underset{˙}{\sim})$
103	102	elrlocbasi	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \exists c \in B \exists d \in S y = [⟨c, d⟩] \underset{˙}{\sim}$
104	101 103	r19.29vva	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x +_{L} y \in ((B \times S) / \underset{˙}{\sim})$
105		simplr	$⊢ ((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x \in ((B \times S) / \underset{˙}{\sim})$
106	105	elrlocbasi	$⊢ ((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \to \exists a \in B \exists b \in S x = [⟨a, b⟩] \underset{˙}{\sim}$
107	104 106	r19.29vva	$⊢ ((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x +_{L} y \in ((B \times S) / \underset{˙}{\sim})$
108	107	3impa	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x +_{L} y \in ((B \times S) / \underset{˙}{\sim})$
109	6	ad10antr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to R \in CRing$
110	109	crnggrpd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to R \in Grp$
111	21	ad10antr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to R \in Ring$
112		simp-9r	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to a \in B$
113	7	ad10antr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to S \in SubMnd ({mulGrp}_{R})$
114	113 13	syl	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to S \subseteq B$
115		simp-5r	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to d \in S$
116	114 115	sseldd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to d \in B$
117	1 2 111 112 116	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} d \in B$
118		simplr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \in S$
119	114 118	sseldd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \in B$
120	1 2 111 117 119	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f \in B$
121		simp-6r	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to c \in B$
122		simp-8r	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \in S$
123	114 122	sseldd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \in B$
124	1 2 111 121 123	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to c \underset{˙}{\cdot} b \in B$
125	1 2 111 124 119	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f \in B$
126		simpllr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to e \in B$
127	1 2 111 123 116	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} d \in B$
128	1 2 111 126 127	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d) \in B$
129	1 3 110 120 125 128	grpassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f)) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{+} (((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)))$
130	1 2 111 112 116 119	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f = a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)$
131	1 2 109 121 123 119	cringmul32d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f = (c \underset{˙}{\cdot} f) \underset{˙}{\cdot} b$
132	1 2 109 126 123 116	crng12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d) = b \underset{˙}{\cdot} (e \underset{˙}{\cdot} d)$
133	1 2 111 126 116	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to e \underset{˙}{\cdot} d \in B$
134	1 2 109 123 133	crngcomd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (e \underset{˙}{\cdot} d) = (e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b$
135	132 134	eqtrd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d) = (e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b$
136	131 135	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = ((c \underset{˙}{\cdot} f) \underset{˙}{\cdot} b) \underset{˙}{+} ((e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b)$
137	130 136	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{+} (((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d))) = (a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{\cdot} b) \underset{˙}{+} ((e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b))$
138	129 137	eqtrd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f)) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = (a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{\cdot} b) \underset{˙}{+} ((e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b))$
139	1 3 2 111 117 124 119	ringdird	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} f = ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f)$
140	139	oveq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} f)) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d))$
141	1 2 111 121 119	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to c \underset{˙}{\cdot} f \in B$
142	1 3 2 111 141 133 123	ringdird	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \underset{˙}{\cdot} b = ((c \underset{˙}{\cdot} f) \underset{˙}{\cdot} b) \underset{˙}{+} ((e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b)$
143	142	oveq2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \underset{˙}{\cdot} b) = (a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{\cdot} b) \underset{˙}{+} ((e \underset{˙}{\cdot} d) \underset{˙}{\cdot} b))$
144	138 140 143	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = (a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \underset{˙}{\cdot} b)$
145	1 2 111 123 116 119	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f = b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)$
146	144 145	opeq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨(((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩ = ⟨(a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \underset{˙}{\cdot} b), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩$
147	146	eceq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨(((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \underset{˙}{\cdot} b), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
148	1 3 110 117 124	grpcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b) \in B$
149	95 113 122 115	submcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} d \in S$
150	1 2 3 4 5 109 113 148 126 149 118 20	rlocaddval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨(((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
151	1 3 110 141 133	grpcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d) \in B$
152	95 113 115 118	submcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to d \underset{˙}{\cdot} f \in S$
153	1 2 3 4 5 109 113 112 151 122 152 20	rlocaddval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} (((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \underset{˙}{\cdot} b), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
154	147 150 153	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
155	1 2 3 4 5 109 113 112 121 122 115 20	rlocaddval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim}$
156	155	oveq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}) +_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim}$
157	1 2 3 4 5 109 113 121 126 115 118 20	rlocaddval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
158	157	oveq2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} +_{L} ([⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim}) = [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
159	154 156 158	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}) +_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} +_{L} ([⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim})$
160		simp-7r	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x = [⟨a, b⟩] \underset{˙}{\sim}$
161		simp-4r	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to y = [⟨c, d⟩] \underset{˙}{\sim}$
162	160 161	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x +_{L} y = [⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}$
163		simpr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to z = [⟨e, f⟩] \underset{˙}{\sim}$
164	162 163	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x +_{L} y) +_{L} z = ([⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}) +_{L} [⟨e, f⟩] \underset{˙}{\sim}$
165	161 163	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to y +_{L} z = [⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim}$
166	160 165	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x +_{L} (y +_{L} z) = [⟨a, b⟩] \underset{˙}{\sim} +_{L} ([⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim})$
167	159 164 166	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x +_{L} y) +_{L} z = x +_{L} (y +_{L} z)$
168		simpr3	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to z \in ((B \times S) / \underset{˙}{\sim})$
169	168	ad6antr	$⊢ (((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to z \in ((B \times S) / \underset{˙}{\sim})$
170	169	elrlocbasi	$⊢ (((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to \exists e \in B \exists f \in S z = [⟨e, f⟩] \underset{˙}{\sim}$
171	167 170	r19.29vva	$⊢ (((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to (x +_{L} y) +_{L} z = x +_{L} (y +_{L} z)$
172		simpr2	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to y \in ((B \times S) / \underset{˙}{\sim})$
173	172	ad5ant12	$⊢ ((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to y \in ((B \times S) / \underset{˙}{\sim})$
174	173	elrlocbasi	$⊢ ((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \exists c \in B \exists d \in S y = [⟨c, d⟩] \underset{˙}{\sim}$
175	171 174	r19.29vva	$⊢ ((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (x +_{L} y) +_{L} z = x +_{L} (y +_{L} z)$
176		simpr1	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to x \in ((B \times S) / \underset{˙}{\sim})$
177	176	elrlocbasi	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to \exists a \in B \exists b \in S x = [⟨a, b⟩] \underset{˙}{\sim}$
178	175 177	r19.29vva	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to (x +_{L} y) +_{L} z = x +_{L} (y +_{L} z)$
179	15 16 108 178 31 61 74	ismndd	$⊢ φ \to L \in Mnd$
180		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
181	1 180 47 43	grpinvcld	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to {inv}_{g} (R) (a) \in B$
182	181 40	opelxpd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨{inv}_{g} (R) (a), b⟩ \in (B \times S)$
183	29	ecelqsi	$⊢ ⟨{inv}_{g} (R) (a), b⟩ \in (B \times S) \to [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
184	182 183	syl	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
185		simpr	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land u = [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim}) \to u = [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim}$
186		simplr	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land u = [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim}) \to x = [⟨a, b⟩] \underset{˙}{\sim}$
187	185 186	oveq12d	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land u = [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim}) \to u +_{L} x = [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim}$
188	187	eqeq1d	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land u = [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim}) \to (u +_{L} x = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim} \leftrightarrow [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim})$
189	1 2 3 4 5 53 38 181 43 40 40 20	rlocaddval	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨({inv}_{g} (R) (a) \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} b), b \underset{˙}{\cdot} b⟩] \underset{˙}{\sim}$
190	1 3 8 180 47 43	grplinvd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to {inv}_{g} (R) (a) \underset{˙}{+} a = 0_{R}$
191	190	oveq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ({inv}_{g} (R) (a) \underset{˙}{+} a) \underset{˙}{\cdot} b = 0_{R} \underset{˙}{\cdot} b$
192	1 3 2 37 181 43 41	ringdird	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ({inv}_{g} (R) (a) \underset{˙}{+} a) \underset{˙}{\cdot} b = ({inv}_{g} (R) (a) \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} b)$
193	191 192 42	3eqtr3d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ({inv}_{g} (R) (a) \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} b) = 0_{R}$
194	193	opeq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨({inv}_{g} (R) (a) \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} b), b \underset{˙}{\cdot} b⟩ = ⟨0_{R}, b \underset{˙}{\cdot} b⟩$
195	194	eceq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨({inv}_{g} (R) (a) \underset{˙}{\cdot} b) \underset{˙}{+} (a \underset{˙}{\cdot} b), b \underset{˙}{\cdot} b⟩] \underset{˙}{\sim} = [⟨0_{R}, b \underset{˙}{\cdot} b⟩] \underset{˙}{\sim}$
196	1 8 24 2 9 10 5 6 7	erler	$⊢ φ \to \underset{˙}{\sim} Er (B \times S)$
197	196	ad4antr	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \underset{˙}{\sim} Er (B \times S)$
198		eqidd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨0_{R}, b \underset{˙}{\cdot} b⟩ = ⟨0_{R}, b \underset{˙}{\cdot} b⟩$
199		eqidd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨0_{R}, 1_{R}⟩ = ⟨0_{R}, 1_{R}⟩$
200	95 38 40 40	submcld	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} b \in S$
201	1 2 24 37 54	ringridmd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 0_{R} \underset{˙}{\cdot} 1_{R} = 0_{R}$
202	39 200	sseldd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} b \in B$
203	1 2 8 37 202	ringlzd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 0_{R} \underset{˙}{\cdot} (b \underset{˙}{\cdot} b) = 0_{R}$
204	201 203	oveq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (0_{R} \underset{˙}{\cdot} 1_{R}) -_{R} (0_{R} \underset{˙}{\cdot} (b \underset{˙}{\cdot} b)) = 0_{R} -_{R} 0_{R}$
205	1 8 9	grpsubid	$⊢ (R \in Grp \land 0_{R} \in B) \to 0_{R} -_{R} 0_{R} = 0_{R}$
206	47 54 205	syl2anc	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 0_{R} -_{R} 0_{R} = 0_{R}$
207	204 206	eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (0_{R} \underset{˙}{\cdot} 1_{R}) -_{R} (0_{R} \underset{˙}{\cdot} (b \underset{˙}{\cdot} b)) = 0_{R}$
208	207	oveq2d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} b) \underset{˙}{\cdot} ((0_{R} \underset{˙}{\cdot} 1_{R}) -_{R} (0_{R} \underset{˙}{\cdot} (b \underset{˙}{\cdot} b))) = (b \underset{˙}{\cdot} b) \underset{˙}{\cdot} 0_{R}$
209	1 2 8 37 202	ringrzd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} b) \underset{˙}{\cdot} 0_{R} = 0_{R}$
210	208 209	eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} b) \underset{˙}{\cdot} ((0_{R} \underset{˙}{\cdot} 1_{R}) -_{R} (0_{R} \underset{˙}{\cdot} (b \underset{˙}{\cdot} b))) = 0_{R}$
211	1 5 39 8 2 9 198 199 54 54 200 55 200 210	erlbrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨0_{R}, b \underset{˙}{\cdot} b⟩ \underset{˙}{\sim} ⟨0_{R}, 1_{R}⟩$
212	197 211	erthi	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨0_{R}, b \underset{˙}{\cdot} b⟩] \underset{˙}{\sim} = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim}$
213	189 195 212	3eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨{inv}_{g} (R) (a), b⟩] \underset{˙}{\sim} +_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim}$
214	184 188 213	rspcedvd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to \exists u \in ((B \times S) / \underset{˙}{\sim}) u +_{L} x = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim}$
215	214 60	r19.29vva	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to \exists u \in ((B \times S) / \underset{˙}{\sim}) u +_{L} x = [⟨0_{R}, 1_{R}⟩] \underset{˙}{\sim}$
216	15 16 76 179 215	isgrpd2e	$⊢ φ \to L \in Grp$
217	77 78	oveq12d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x \cdot_{L} y = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}$
218		eqid	$⊢ \cdot_{L} = \cdot_{L}$
219	1 2 3 4 5 80 81 82 83 84 85 218	rlocmulval	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim}$
220	1 2 88 82 83	ringcld	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} c \in B$
221	220 96	opelxpd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to ⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩ \in (B \times S)$
222	29	ecelqsi	$⊢ ⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩ \in (B \times S) \to [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
223	221 222	syl	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
224	219 223	eqeltrd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
225	217 224	eqeltrd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x \cdot_{L} y \in ((B \times S) / \underset{˙}{\sim})$
226	225 103	r19.29vva	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} y \in ((B \times S) / \underset{˙}{\sim})$
227	226 106	r19.29vva	$⊢ ((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x \cdot_{L} y \in ((B \times S) / \underset{˙}{\sim})$
228	227	3impa	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x \cdot_{L} y \in ((B \times S) / \underset{˙}{\sim})$
229	1 2 111 112 121 126	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} c) \underset{˙}{\cdot} e = a \underset{˙}{\cdot} (c \underset{˙}{\cdot} e)$
230	229 145	opeq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨(a \underset{˙}{\cdot} c) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩ = ⟨a \underset{˙}{\cdot} (c \underset{˙}{\cdot} e), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩$
231	230	eceq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨(a \underset{˙}{\cdot} c) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} (c \underset{˙}{\cdot} e), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
232	1 2 111 112 121	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} c \in B$
233	1 2 3 4 5 109 113 232 126 149 118 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} c) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
234	1 2 111 121 126	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to c \underset{˙}{\cdot} e \in B$
235	1 2 3 4 5 109 113 112 234 122 152 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} (c \underset{˙}{\cdot} e), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
236	231 233 235	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
237	1 2 3 4 5 109 113 112 121 122 115 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim}$
238	237	oveq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}) \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}$
239	1 2 3 4 5 109 113 121 126 115 118 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
240	239	oveq2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} ([⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}) = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
241	236 238 240	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}) \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} ([⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim})$
242	160 161	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x \cdot_{L} y = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}$
243	242 163	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x \cdot_{L} y) \cdot_{L} z = ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}) \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}$
244	161 163	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to y \cdot_{L} z = [⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}$
245	160 244	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x \cdot_{L} (y \cdot_{L} z) = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} ([⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim})$
246	241 243 245	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x \cdot_{L} y) \cdot_{L} z = x \cdot_{L} (y \cdot_{L} z)$
247	246 170	r19.29vva	$⊢ (((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to (x \cdot_{L} y) \cdot_{L} z = x \cdot_{L} (y \cdot_{L} z)$
248	247 174	r19.29vva	$⊢ ((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (x \cdot_{L} y) \cdot_{L} z = x \cdot_{L} (y \cdot_{L} z)$
249	248 177	r19.29vva	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to (x \cdot_{L} y) \cdot_{L} z = x \cdot_{L} (y \cdot_{L} z)$
250	196	ad10antr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to \underset{˙}{\sim} Er (B \times S)$
251		eqidd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩ = ⟨a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩$
252	1 2 111 112 123	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} b \in B$
253	1 3 2 111 252 141 133	ringdid	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} b) \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) = ((a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (c \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (e \underset{˙}{\cdot} d))$
254	1 2 111 112 123 151	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} b) \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)))$
255	253 254	eqtr3d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (c \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (e \underset{˙}{\cdot} d)) = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)))$
256	11	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
257	6 256	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
258	257	ad10antr	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to {mulGrp}_{R} \in CMnd$
259	12 95 258 112 121 123 119	cmn4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f) = (a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (c \underset{˙}{\cdot} f)$
260	12 95 258 112 126 123 116	cmn4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d) = (a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (e \underset{˙}{\cdot} d)$
261	259 260	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = ((a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (c \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} b) \underset{˙}{\cdot} (e \underset{˙}{\cdot} d))$
262	1 2 109 123 112 151	crng12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d))) = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)))$
263	255 261 262	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)) = b \underset{˙}{\cdot} (a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)))$
264	1 2 109 127 123 119	crng12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f) = b \underset{˙}{\cdot} ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f)$
265	145	oveq2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) = b \underset{˙}{\cdot} (b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f))$
266	264 265	eqtrd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f) = b \underset{˙}{\cdot} (b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f))$
267	263 266	opeq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨((a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)⟩ = ⟨b \underset{˙}{\cdot} (a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d))), b \underset{˙}{\cdot} (b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f))⟩$
268	1 2 111 112 151	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)) \in B$
269	1 2 111 123 268	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d))) \in B$
270	95 113 122 152	submcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f) \in S$
271	95 113 122 270	submcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \in S$
272		eqidd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d))) = b \underset{˙}{\cdot} (a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)))$
273		eqidd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} (b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) = b \underset{˙}{\cdot} (b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f))$
274	1 5 109 113 2 251 267 268 269 270 271 122 272 273	erlbr2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩ \underset{˙}{\sim} ⟨((a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)⟩$
275	250 274	erthi	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim} = [⟨((a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
276	1 2 3 4 5 109 113 112 151 122 152 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} ((c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d)), b \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
277	1 2 111 112 126	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} e \in B$
278	95 113 122 118	submcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} f \in S$
279	1 2 3 4 5 109 113 232 277 149 278 20	rlocaddval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} +_{L} [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨((a \underset{˙}{\cdot} c) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{+} ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} d)), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
280	275 276 279	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} +_{L} [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
281	157	oveq2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} ([⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim}) = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨(c \underset{˙}{\cdot} f) \underset{˙}{+} (e \underset{˙}{\cdot} d), d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
282	1 2 3 4 5 109 113 112 126 122 118 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
283	237 282	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}) +_{L} ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}) = [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} +_{L} [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
284	280 281 283	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} ([⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim}) = ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}) +_{L} ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim})$
285	160 165	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x \cdot_{L} (y +_{L} z) = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} ([⟨c, d⟩] \underset{˙}{\sim} +_{L} [⟨e, f⟩] \underset{˙}{\sim})$
286	160 163	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x \cdot_{L} z = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}$
287	242 286	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x \cdot_{L} y) +_{L} (x \cdot_{L} z) = ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim}) +_{L} ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim})$
288	284 285 287	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to x \cdot_{L} (y +_{L} z) = (x \cdot_{L} y) +_{L} (x \cdot_{L} z)$
289	288 170	r19.29vva	$⊢ (((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x \cdot_{L} (y +_{L} z) = (x \cdot_{L} y) +_{L} (x \cdot_{L} z)$
290	289 174	r19.29vva	$⊢ ((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} (y +_{L} z) = (x \cdot_{L} y) +_{L} (x \cdot_{L} z)$
291	290 177	r19.29vva	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to x \cdot_{L} (y +_{L} z) = (x \cdot_{L} y) +_{L} (x \cdot_{L} z)$
292	1 3 2 111 117 124 126	ringdird	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} e = ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e)$
293	292	opeq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩ = ⟨((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e), (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩$
294	1 2 111 117 126 119	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{\cdot} f = (a \underset{˙}{\cdot} d) \underset{˙}{\cdot} (e \underset{˙}{\cdot} f)$
295	1 2 111 117 126	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e \in B$
296	1 2 109 119 295	crngcomd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \underset{˙}{\cdot} ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) = ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{\cdot} f$
297	12 95 258 112 126 116 119	cmn4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f) = (a \underset{˙}{\cdot} d) \underset{˙}{\cdot} (e \underset{˙}{\cdot} f)$
298	294 296 297	3eqtr4rd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f) = f \underset{˙}{\cdot} ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e)$
299	1 2 111 124 126 119	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e) \underset{˙}{\cdot} f = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} (e \underset{˙}{\cdot} f)$
300	1 2 111 124 126	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e \in B$
301	1 2 109 119 300	crngcomd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \underset{˙}{\cdot} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e) = ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e) \underset{˙}{\cdot} f$
302	12 95 258 121 126 123 119	cmn4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f) = (c \underset{˙}{\cdot} b) \underset{˙}{\cdot} (e \underset{˙}{\cdot} f)$
303	299 301 302	3eqtr4rd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f) = f \underset{˙}{\cdot} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e)$
304	298 303	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} ((c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) = (f \underset{˙}{\cdot} ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e)) \underset{˙}{+} (f \underset{˙}{\cdot} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e))$
305	1 3 2 111 119 295 300	ringdid	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \underset{˙}{\cdot} (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e)) = (f \underset{˙}{\cdot} ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e)) \underset{˙}{+} (f \underset{˙}{\cdot} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e))$
306	304 305	eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} ((c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) = f \underset{˙}{\cdot} (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e))$
307	114 278	sseldd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} f \in B$
308	1 2 111 116 307 119	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (d \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{\cdot} f = d \underset{˙}{\cdot} ((b \underset{˙}{\cdot} f) \underset{˙}{\cdot} f)$
309	1 2 109 123 116	crngcomd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} d = d \underset{˙}{\cdot} b$
310	309	oveq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f = (d \underset{˙}{\cdot} b) \underset{˙}{\cdot} f$
311	1 2 111 116 123 119	ringassd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (d \underset{˙}{\cdot} b) \underset{˙}{\cdot} f = d \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)$
312	310 311	eqtrd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f = d \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)$
313	312	oveq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{\cdot} f = (d \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)) \underset{˙}{\cdot} f$
314	1 2 109 307 116 119	crng12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} f) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f) = d \underset{˙}{\cdot} ((b \underset{˙}{\cdot} f) \underset{˙}{\cdot} f)$
315	308 313 314	3eqtr4rd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} f) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f) = ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{\cdot} f$
316	306 315	opeq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} ((c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)), (b \underset{˙}{\cdot} f) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩ = ⟨f \underset{˙}{\cdot} (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e)), ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{\cdot} f⟩$
317	1 3 110 295 300	grpcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e) \in B$
318	1 2 111 119 317	ringcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \underset{˙}{\cdot} (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e)) \in B$
319	145 270	eqeltrd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f \in S$
320	95 113 319 118	submcld	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{\cdot} f \in S$
321		eqidd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to f \underset{˙}{\cdot} (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e)) = f \underset{˙}{\cdot} (((a \underset{˙}{\cdot} d) \underset{˙}{\cdot} e) \underset{˙}{+} ((c \underset{˙}{\cdot} b) \underset{˙}{\cdot} e))$
322	114 319	sseldd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f \in B$
323	1 2 109 322 119	crngcomd	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f) \underset{˙}{\cdot} f = f \underset{˙}{\cdot} ((b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f)$
324	1 5 109 113 2 293 316 317 318 319 320 118 321 323	erlbr2d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ⟨((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩ \underset{˙}{\sim} ⟨((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} ((c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)), (b \underset{˙}{\cdot} f) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩$
325	250 324	erthi	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} ((c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)), (b \underset{˙}{\cdot} f) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
326	1 2 3 4 5 109 113 148 126 149 118 218	rlocmulval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨((a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b)) \underset{˙}{\cdot} e, (b \underset{˙}{\cdot} d) \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
327	1 2 3 4 5 109 113 277 234 278 152 20	rlocaddval	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} +_{L} [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} = [⟨((a \underset{˙}{\cdot} e) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)) \underset{˙}{+} ((c \underset{˙}{\cdot} e) \underset{˙}{\cdot} (b \underset{˙}{\cdot} f)), (b \underset{˙}{\cdot} f) \underset{˙}{\cdot} (d \underset{˙}{\cdot} f)⟩] \underset{˙}{\sim}$
328	325 326 327	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} +_{L} [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
329	155	oveq1d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}) \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = [⟨(a \underset{˙}{\cdot} d) \underset{˙}{+} (c \underset{˙}{\cdot} b), b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}$
330	282 239	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}) +_{L} ([⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}) = [⟨a \underset{˙}{\cdot} e, b \underset{˙}{\cdot} f⟩] \underset{˙}{\sim} +_{L} [⟨c \underset{˙}{\cdot} e, d \underset{˙}{\cdot} f⟩] \underset{˙}{\sim}$
331	328 329 330	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to ([⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}) \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim} = ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}) +_{L} ([⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim})$
332	162 163	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x +_{L} y) \cdot_{L} z = ([⟨a, b⟩] \underset{˙}{\sim} +_{L} [⟨c, d⟩] \underset{˙}{\sim}) \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}$
333	286 244	oveq12d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x \cdot_{L} z) +_{L} (y \cdot_{L} z) = ([⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim}) +_{L} ([⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨e, f⟩] \underset{˙}{\sim})$
334	331 332 333	3eqtr4d	$⊢ ((((((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \land e \in B) \land f \in S) \land z = [⟨e, f⟩] \underset{˙}{\sim}) \to (x +_{L} y) \cdot_{L} z = (x \cdot_{L} z) +_{L} (y \cdot_{L} z)$
335	334 170	r19.29vva	$⊢ (((((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to (x +_{L} y) \cdot_{L} z = (x \cdot_{L} z) +_{L} (y \cdot_{L} z)$
336	335 174	r19.29vva	$⊢ ((((φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to (x +_{L} y) \cdot_{L} z = (x \cdot_{L} z) +_{L} (y \cdot_{L} z)$
337	336 177	r19.29vva	$⊢ (φ \land (x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim}) \land z \in ((B \times S) / \underset{˙}{\sim}))) \to (x +_{L} y) \cdot_{L} z = (x \cdot_{L} z) +_{L} (y \cdot_{L} z)$
338	14 27	sseldd	$⊢ φ \to 1_{R} \in B$
339	338 27	opelxpd	$⊢ φ \to ⟨1_{R}, 1_{R}⟩ \in (B \times S)$
340	29	ecelqsi	$⊢ ⟨1_{R}, 1_{R}⟩ \in (B \times S) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
341	339 340	syl	$⊢ φ \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \in ((B \times S) / \underset{˙}{\sim})$
342	35	oveq2d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim}$
343	1 2 24 37 43	ringlidmd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 1_{R} \underset{˙}{\cdot} a = a$
344	343 50	opeq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨1_{R} \underset{˙}{\cdot} a, 1_{R} \underset{˙}{\cdot} b⟩ = ⟨a, b⟩$
345	344	eceq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨1_{R} \underset{˙}{\cdot} a, 1_{R} \underset{˙}{\cdot} b⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
346	39 55	sseldd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to 1_{R} \in B$
347	1 2 3 4 5 53 38 346 43 55 40 218	rlocmulval	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨1_{R} \underset{˙}{\cdot} a, 1_{R} \underset{˙}{\cdot} b⟩] \underset{˙}{\sim}$
348	345 347 35	3eqtr4d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim} = x$
349	342 348	eqtrd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = x$
350	349 60	r19.29vva	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} \cdot_{L} x = x$
351	1 2 3 4 5 53 38 43 346 40 55 218	rlocmulval	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} 1_{R}, b \underset{˙}{\cdot} 1_{R}⟩] \underset{˙}{\sim}$
352	35	oveq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim}$
353	44	eqcomd	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to a = a \underset{˙}{\cdot} 1_{R}$
354	353 69	opeq12d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to ⟨a, b⟩ = ⟨a \underset{˙}{\cdot} 1_{R}, b \underset{˙}{\cdot} 1_{R}⟩$
355	354	eceq1d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} = [⟨a \underset{˙}{\cdot} 1_{R}, b \underset{˙}{\cdot} 1_{R}⟩] \underset{˙}{\sim}$
356	351 352 355	3eqtr4d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
357	356 35	eqtr4d	$⊢ ((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = x$
358	357 60	r19.29vva	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim})) \to x \cdot_{L} [⟨1_{R}, 1_{R}⟩] \underset{˙}{\sim} = x$
359	1 2 80 82 83	crngcomd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to a \underset{˙}{\cdot} c = c \underset{˙}{\cdot} a$
360	1 2 80 92 90	crngcomd	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to b \underset{˙}{\cdot} d = d \underset{˙}{\cdot} b$
361	359 360	opeq12d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to ⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩ = ⟨c \underset{˙}{\cdot} a, d \underset{˙}{\cdot} b⟩$
362	361	eceq1d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a \underset{˙}{\cdot} c, b \underset{˙}{\cdot} d⟩] \underset{˙}{\sim} = [⟨c \underset{˙}{\cdot} a, d \underset{˙}{\cdot} b⟩] \underset{˙}{\sim}$
363	1 2 3 4 5 80 81 83 82 85 84 218	rlocmulval	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim} = [⟨c \underset{˙}{\cdot} a, d \underset{˙}{\cdot} b⟩] \underset{˙}{\sim}$
364	362 219 363	3eqtr4d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to [⟨a, b⟩] \underset{˙}{\sim} \cdot_{L} [⟨c, d⟩] \underset{˙}{\sim} = [⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim}$
365	78 77	oveq12d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to y \cdot_{L} x = [⟨c, d⟩] \underset{˙}{\sim} \cdot_{L} [⟨a, b⟩] \underset{˙}{\sim}$
366	364 217 365	3eqtr4d	$⊢ ((((((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \land c \in B) \land d \in S) \land y = [⟨c, d⟩] \underset{˙}{\sim}) \to x \cdot_{L} y = y \cdot_{L} x$
367	366 103	r19.29vva	$⊢ (((((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \land a \in B) \land b \in S) \land x = [⟨a, b⟩] \underset{˙}{\sim}) \to x \cdot_{L} y = y \cdot_{L} x$
368	367 106	r19.29vva	$⊢ ((φ \land x \in ((B \times S) / \underset{˙}{\sim})) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x \cdot_{L} y = y \cdot_{L} x$
369	368	3impa	$⊢ (φ \land x \in ((B \times S) / \underset{˙}{\sim}) \land y \in ((B \times S) / \underset{˙}{\sim})) \to x \cdot_{L} y = y \cdot_{L} x$
370	15 16 17 216 228 249 291 337 341 350 358 369	iscrngd	$⊢ φ \to L \in CRing$

Metamath Proof Explorer

Theorem rloccring

Proof