erler

Description: The relation used to build the ring localization is an equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erler.1	$⊢ B = {Base}_{R}$
	erler.2	$⊢ \underset{˙}{0} = 0_{R}$
	erler.3	$⊢ \underset{˙}{1} = 1_{R}$
	erler.4	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	erler.5	$⊢ \underset{˙}{-} = -_{R}$
	erler.w	$⊢ W = B \times S$
	erler.q	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	erler.r	$⊢ φ \to R \in CRing$
	erler.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
Assertion	erler	$⊢ φ \to \underset{˙}{\sim} Er W$

Proof

Step	Hyp	Ref	Expression
1		erler.1	$⊢ B = {Base}_{R}$
2		erler.2	$⊢ \underset{˙}{0} = 0_{R}$
3		erler.3	$⊢ \underset{˙}{1} = 1_{R}$
4		erler.4	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		erler.5	$⊢ \underset{˙}{-} = -_{R}$
6		erler.w	$⊢ W = B \times S$
7		erler.q	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
8		erler.r	$⊢ φ \to R \in CRing$
9		erler.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
10		eqid	$⊢ \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\} = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
11	10	relopabiv	$⊢ Rel \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
12	11	a1i	$⊢ φ \to Rel \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
13		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
14	13 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
15	14	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq B$
16	9 15	syl	$⊢ φ \to S \subseteq B$
17	1 2 4 5 6 10 16	erlval	$⊢ φ \to R ~_{RL} S = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
18	7 17	eqtrid	$⊢ φ \to \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
19	18	releqd	$⊢ φ \to (Rel \underset{˙}{\sim} \leftrightarrow Rel \{⟨a, b⟩ \| ((a \in W \land b \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\})$
20	12 19	mpbird	$⊢ φ \to Rel \underset{˙}{\sim}$
21		simpl	$⊢ (a = x \land b = y) \to a = x$
22	21	fveq2d	$⊢ (a = x \land b = y) \to 1^{st} (a) = 1^{st} (x)$
23		simpr	$⊢ (a = x \land b = y) \to b = y$
24	23	fveq2d	$⊢ (a = x \land b = y) \to 2^{nd} (b) = 2^{nd} (y)$
25	22 24	oveq12d	$⊢ (a = x \land b = y) \to 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b) = 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)$
26	23	fveq2d	$⊢ (a = x \land b = y) \to 1^{st} (b) = 1^{st} (y)$
27	21	fveq2d	$⊢ (a = x \land b = y) \to 2^{nd} (a) = 2^{nd} (x)$
28	26 27	oveq12d	$⊢ (a = x \land b = y) \to 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a) = 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)$
29	25 28	oveq12d	$⊢ (a = x \land b = y) \to (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)) = (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))$
30	29	oveq2d	$⊢ (a = x \land b = y) \to t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))$
31	30	eqeq1d	$⊢ (a = x \land b = y) \to (t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
32	31	rexbidv	$⊢ (a = x \land b = y) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
33	32	adantl	$⊢ (φ \land (a = x \land b = y)) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
34	18 33	brab2d	$⊢ φ \to (x \underset{˙}{\sim} y \leftrightarrow ((x \in W \land y \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}))$
35	34	biimpa	$⊢ (φ \land x \underset{˙}{\sim} y) \to ((x \in W \land y \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
36	35	simplrd	$⊢ (φ \land x \underset{˙}{\sim} y) \to y \in W$
37	35	simplld	$⊢ (φ \land x \underset{˙}{\sim} y) \to x \in W$
38	36 37	jca	$⊢ (φ \land x \underset{˙}{\sim} y) \to (y \in W \land x \in W)$
39	35	simprd	$⊢ (φ \land x \underset{˙}{\sim} y) \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
40	8	crngringd	$⊢ φ \to R \in Ring$
41	40	ringgrpd	$⊢ φ \to R \in Grp$
42	41	ad3antrrr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to R \in Grp$
43	40	ad3antrrr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to R \in Ring$
44	37	ad2antrr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to x \in W$
45		xp1st	$⊢ x \in (B \times S) \to 1^{st} (x) \in B$
46	45 6	eleq2s	$⊢ x \in W \to 1^{st} (x) \in B$
47	44 46	syl	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 1^{st} (x) \in B$
48	16	ad3antrrr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to S \subseteq B$
49	36	ad2antrr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to y \in W$
50		xp2nd	$⊢ y \in (B \times S) \to 2^{nd} (y) \in S$
51	50 6	eleq2s	$⊢ y \in W \to 2^{nd} (y) \in S$
52	49 51	syl	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 2^{nd} (y) \in S$
53	48 52	sseldd	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 2^{nd} (y) \in B$
54	1 4 43 47 53	ringcld	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y) \in B$
55		xp1st	$⊢ y \in (B \times S) \to 1^{st} (y) \in B$
56	55 6	eleq2s	$⊢ y \in W \to 1^{st} (y) \in B$
57	49 56	syl	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 1^{st} (y) \in B$
58		xp2nd	$⊢ x \in (B \times S) \to 2^{nd} (x) \in S$
59	58 6	eleq2s	$⊢ x \in W \to 2^{nd} (x) \in S$
60	44 59	syl	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 2^{nd} (x) \in S$
61	48 60	sseldd	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 2^{nd} (x) \in B$
62	1 4 43 57 61	ringcld	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x) \in B$
63		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
64	1 5 63	grpinvsub	$⊢ (R \in Grp \land 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y) \in B \land 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x) \in B) \to {inv}_{g} (R) ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))$
65	42 54 62 64	syl3anc	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to {inv}_{g} (R) ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))$
66	65	oveq2d	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} {inv}_{g} (R) ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)))$
67		simplr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \in S$
68	48 67	sseldd	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \in B$
69	1 5	grpsubcl	$⊢ (R \in Grp \land 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y) \in B \land 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x) \in B) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \in B$
70	42 54 62 69	syl3anc	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \in B$
71	1 4 63 43 68 70	ringmneg2	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} {inv}_{g} (R) ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = {inv}_{g} (R) (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))$
72		simpr	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
73	72	fveq2d	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to {inv}_{g} (R) (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) = {inv}_{g} (R) (\underset{˙}{0})$
74	2 63	grpinvid	$⊢ R \in Grp \to {inv}_{g} (R) (\underset{˙}{0}) = \underset{˙}{0}$
75	42 74	syl	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to {inv}_{g} (R) (\underset{˙}{0}) = \underset{˙}{0}$
76	71 73 75	3eqtrd	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} {inv}_{g} (R) ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
77	66 76	eqtr3d	$⊢ (((φ \land x \underset{˙}{\sim} y) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}$
78	77	ex	$⊢ ((φ \land x \underset{˙}{\sim} y) \land t \in S) \to (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0} \to t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
79	78	reximdva	$⊢ (φ \land x \underset{˙}{\sim} y) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0} \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
80	39 79	mpd	$⊢ (φ \land x \underset{˙}{\sim} y) \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}$
81	38 80	jca	$⊢ (φ \land x \underset{˙}{\sim} y) \to ((y \in W \land x \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
82		simpl	$⊢ (a = y \land b = x) \to a = y$
83	82	fveq2d	$⊢ (a = y \land b = x) \to 1^{st} (a) = 1^{st} (y)$
84		simpr	$⊢ (a = y \land b = x) \to b = x$
85	84	fveq2d	$⊢ (a = y \land b = x) \to 2^{nd} (b) = 2^{nd} (x)$
86	83 85	oveq12d	$⊢ (a = y \land b = x) \to 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b) = 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)$
87	84	fveq2d	$⊢ (a = y \land b = x) \to 1^{st} (b) = 1^{st} (x)$
88	82	fveq2d	$⊢ (a = y \land b = x) \to 2^{nd} (a) = 2^{nd} (y)$
89	87 88	oveq12d	$⊢ (a = y \land b = x) \to 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a) = 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)$
90	86 89	oveq12d	$⊢ (a = y \land b = x) \to (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)) = (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))$
91	90	oveq2d	$⊢ (a = y \land b = x) \to t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)))$
92	91	eqeq1d	$⊢ (a = y \land b = x) \to (t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
93	92	rexbidv	$⊢ (a = y \land b = x) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
94	93	adantl	$⊢ (φ \land (a = y \land b = x)) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
95	18 94	brab2d	$⊢ φ \to (y \underset{˙}{\sim} x \leftrightarrow ((y \in W \land x \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}))$
96	95	adantr	$⊢ (φ \land x \underset{˙}{\sim} y) \to (y \underset{˙}{\sim} x \leftrightarrow ((y \in W \land x \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}))$
97	81 96	mpbird	$⊢ (φ \land x \underset{˙}{\sim} y) \to y \underset{˙}{\sim} x$
98	9	ad6antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to S \in SubMnd ({mulGrp}_{R})$
99	98 15	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to S \subseteq B$
100	37	adantr	$⊢ ((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \to x \in W$
101	100	ad4antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to x \in W$
102	101 6	eleqtrdi	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to x \in (B \times S)$
103		1st2nd2	$⊢ x \in (B \times S) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
104	102 103	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
105		simpl	$⊢ (a = y \land b = z) \to a = y$
106	105	fveq2d	$⊢ (a = y \land b = z) \to 1^{st} (a) = 1^{st} (y)$
107		simpr	$⊢ (a = y \land b = z) \to b = z$
108	107	fveq2d	$⊢ (a = y \land b = z) \to 2^{nd} (b) = 2^{nd} (z)$
109	106 108	oveq12d	$⊢ (a = y \land b = z) \to 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b) = 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)$
110	107	fveq2d	$⊢ (a = y \land b = z) \to 1^{st} (b) = 1^{st} (z)$
111	105	fveq2d	$⊢ (a = y \land b = z) \to 2^{nd} (a) = 2^{nd} (y)$
112	110 111	oveq12d	$⊢ (a = y \land b = z) \to 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a) = 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)$
113	109 112	oveq12d	$⊢ (a = y \land b = z) \to (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)) = (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))$
114	113	oveq2d	$⊢ (a = y \land b = z) \to t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
115	114	eqeq1d	$⊢ (a = y \land b = z) \to (t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
116	115	rexbidv	$⊢ (a = y \land b = z) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
117		oveq1	$⊢ t = u \to t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
118	117	eqeq1d	$⊢ t = u \to (t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0} \leftrightarrow u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
119	118	cbvrexvw	$⊢ \exists t \in S t \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0} \leftrightarrow \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}$
120	116 119	bitrdi	$⊢ (a = y \land b = z) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
121	120	adantl	$⊢ (φ \land (a = y \land b = z)) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
122	18 121	brab2d	$⊢ φ \to (y \underset{˙}{\sim} z \leftrightarrow ((y \in W \land z \in W) \land \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}))$
123	122	biimpa	$⊢ (φ \land y \underset{˙}{\sim} z) \to ((y \in W \land z \in W) \land \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
124	123	adantlr	$⊢ ((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \to ((y \in W \land z \in W) \land \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0})$
125	124	simplrd	$⊢ ((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \to z \in W$
126	125	ad4antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to z \in W$
127	126 6	eleqtrdi	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to z \in (B \times S)$
128		1st2nd2	$⊢ z \in (B \times S) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
129	127 128	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
130	101 46	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (x) \in B$
131		xp1st	$⊢ z \in (B \times S) \to 1^{st} (z) \in B$
132	131 6	eleq2s	$⊢ z \in W \to 1^{st} (z) \in B$
133	126 132	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (z) \in B$
134	101 59	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (x) \in S$
135		xp2nd	$⊢ z \in (B \times S) \to 2^{nd} (z) \in S$
136	135 6	eleq2s	$⊢ z \in W \to 2^{nd} (z) \in S$
137	126 136	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \in S$
138		simp-4r	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to t \in S$
139		simplr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to u \in S$
140	13 4	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
141	140	submcl	$⊢ (S \in SubMnd ({mulGrp}_{R}) \land t \in S \land u \in S) \to t \underset{˙}{\cdot} u \in S$
142	98 138 139 141	syl3anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} u \in S$
143	36	ad5antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to y \in W$
144	143 51	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \in S$
145	140	submcl	$⊢ (S \in SubMnd ({mulGrp}_{R}) \land t \underset{˙}{\cdot} u \in S \land 2^{nd} (y) \in S) \to (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (y) \in S$
146	98 142 144 145	syl3anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (y) \in S$
147	40	ad6antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to R \in Ring$
148	99 144	sseldd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \in B$
149	99 137	sseldd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \in B$
150	1 4 147 130 149	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z) \in B$
151	99 134	sseldd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (x) \in B$
152	1 4 147 133 151	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x) \in B$
153	1 4 5 147 148 150 152	ringsubdi	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))) = (2^{nd} (y) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z))) \underset{˙}{-} (2^{nd} (y) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x)))$
154	8	ad6antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to R \in CRing$
155	1 4 154 148 130 149	crng12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) = 1^{st} (x) \underset{˙}{\cdot} (2^{nd} (y) \underset{˙}{\cdot} 2^{nd} (z))$
156	1 4 154 148 149	crngcomd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} 2^{nd} (z) = 2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (y)$
157	156	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (x) \underset{˙}{\cdot} (2^{nd} (y) \underset{˙}{\cdot} 2^{nd} (z)) = 1^{st} (x) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (y))$
158	1 4 154 130 149 148	crng12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (x) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (y)) = 2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))$
159	155 157 158	3eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) = 2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))$
160	1 4 154 148 133 151	crng12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x)) = 1^{st} (z) \underset{˙}{\cdot} (2^{nd} (y) \underset{˙}{\cdot} 2^{nd} (x))$
161	1 4 154 148 151	crngcomd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} 2^{nd} (x) = 2^{nd} (x) \underset{˙}{\cdot} 2^{nd} (y)$
162	161	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (z) \underset{˙}{\cdot} (2^{nd} (y) \underset{˙}{\cdot} 2^{nd} (x)) = 1^{st} (z) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} 2^{nd} (y))$
163	1 4 154 133 151 148	crng12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (z) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} 2^{nd} (y)) = 2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))$
164	160 162 163	3eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x)) = 2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))$
165	159 164	oveq12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (2^{nd} (y) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z))) \underset{˙}{-} (2^{nd} (y) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))) = (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
166	1 4 147 130 148	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y) \in B$
167	143 56	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \in B$
168	1 4 147 167 151	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x) \in B$
169	1 4 5 147 149 166 168	ringsubdi	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))$
170	1 4 147 167 149	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z) \in B$
171	1 4 147 133 148	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y) \in B$
172	1 4 5 147 151 170 171	ringsubdi	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
173	169 172	oveq12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = ((2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} ((2^{nd} (x) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
174	1 4 154 167 149 151	crng12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)) = 2^{nd} (z) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))$
175	174	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x))) = (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))$
176	1 4 154 149 151	crngcomd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x) = 2^{nd} (x) \underset{˙}{\cdot} 2^{nd} (z)$
177	176	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)) = 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} 2^{nd} (z))$
178	1 4 154 151 167 149	crng12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (x) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) = 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} 2^{nd} (z))$
179	177 178	eqtr4d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)) = 2^{nd} (x) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z))$
180	179	oveq1d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
181	175 180	oveq12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} ((1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = ((2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} ((2^{nd} (x) \underset{˙}{\cdot} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
182	41	ad6antr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to R \in Grp$
183	1 4 147 149 166	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \in B$
184	1 4 147 149 151	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x) \in B$
185	1 4 147 167 184	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)) \in B$
186	1 4 147 151 171	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)) \in B$
187		eqid	$⊢ +_{R} = +_{R}$
188	1 187 5	grpnpncan	$⊢ (R \in Grp \land (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \in B \land 1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)) \in B \land 2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)) \in B)) \to ((2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} ((1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
189	182 183 185 186 188	syl13anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} ((1^{st} (y) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} 2^{nd} (x))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
190	173 181 189	3eqtr2rd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (2^{nd} (z) \underset{˙}{\cdot} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y))) \underset{˙}{-} (2^{nd} (x) \underset{˙}{\cdot} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
191	153 165 190	3eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (y) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))) = (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
192	191	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (y) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x)))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} ((2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))))$
193	99 142	sseldd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} u \in B$
194	1 5	grpsubcl	$⊢ (R \in Grp \land 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z) \in B \land 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x) \in B) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x)) \in B$
195	182 150 152 194	syl3anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x)) \in B$
196	1 4 147 193 148 195	ringassd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (y) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))))$
197	99 139	sseldd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to u \in B$
198	99 138	sseldd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to t \in B$
199	1 4 154 197 149 198	cringmul32d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} t = (u \underset{˙}{\cdot} t) \underset{˙}{\cdot} 2^{nd} (z)$
200	1 4 154 197 198	crngcomd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to u \underset{˙}{\cdot} t = t \underset{˙}{\cdot} u$
201	200	oveq1d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} t) \underset{˙}{\cdot} 2^{nd} (z) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (z)$
202	199 201	eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} t = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (z)$
203	202	oveq1d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} t) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))$
204	1 4 147 197 149	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to u \underset{˙}{\cdot} 2^{nd} (z) \in B$
205	182 166 168 69	syl3anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)) \in B$
206	1 4 147 204 198 205	ringassd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} t) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))$
207	1 4 147 193 149 205	ringassd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))$
208	203 206 207	3eqtr3d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))$
209	1 4 154 198 151 197	cringmul32d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} u = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (x)$
210	209	oveq1d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} u) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))$
211	1 4 147 198 151	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} 2^{nd} (x) \in B$
212	1 5	grpsubcl	$⊢ (R \in Grp \land 1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z) \in B \land 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y) \in B) \to (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)) \in B$
213	182 170 171 212	syl3anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)) \in B$
214	1 4 147 211 197 213	ringassd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} u) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
215	1 4 147 193 151 213	ringassd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
216	210 214 215	3eqtr3d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))$
217	208 216	oveq12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))) = ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))))$
218	1 4 147 149 205	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) \in B$
219	1 4 147 151 213	ringcld	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to 2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) \in B$
220	1 187 4	ringdi	$⊢ (R \in Ring \land (t \underset{˙}{\cdot} u \in B \land 2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) \in B \land 2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) \in B)) \to (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} ((2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))) = ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))))$
221	147 193 218 219 220	syl13anc	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} ((2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))) = ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))))$
222	217 221	eqtr4d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))) = (t \underset{˙}{\cdot} u) \underset{˙}{\cdot} ((2^{nd} (z) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) +_{R} (2^{nd} (x) \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))))$
223	192 196 222	3eqtr4d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))) = ((u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))))$
224		simpllr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
225	224	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) = (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} \underset{˙}{0}$
226	1 4 2 147 204	ringrzd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
227	225 226	eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x)))) = \underset{˙}{0}$
228		simpr	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}$
229	228	oveq2d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} \underset{˙}{0}$
230	1 4 2 147 211	ringrzd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
231	229 230	eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to (t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y)))) = \underset{˙}{0}$
232	227 231	oveq12d	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((u \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{\cdot} (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))))) +_{R} ((t \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{\cdot} (u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))))) = \underset{˙}{0} +_{R} \underset{˙}{0}$
233	1 2	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
234	182 233	syl	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to \underset{˙}{0} \in B$
235	1 187 2 182 234	grplidd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
236	223 232 235	3eqtrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to ((t \underset{˙}{\cdot} u) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
237	1 7 99 2 4 5 104 129 130 133 134 137 146 236	erlbrd	$⊢ ((((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \land u \in S) \land u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}) \to x \underset{˙}{\sim} z$
238	124	simprd	$⊢ ((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \to \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}$
239	238	ad2antrr	$⊢ ((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to \exists u \in S u \underset{˙}{\cdot} ((1^{st} (y) \underset{˙}{\cdot} 2^{nd} (z)) \underset{˙}{-} (1^{st} (z) \underset{˙}{\cdot} 2^{nd} (y))) = \underset{˙}{0}$
240	237 239	r19.29a	$⊢ ((((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \to x \underset{˙}{\sim} z$
241	39	adantr	$⊢ ((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (y)) \underset{˙}{-} (1^{st} (y) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
242	240 241	r19.29a	$⊢ ((φ \land x \underset{˙}{\sim} y) \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z$
243	242	anasss	$⊢ (φ \land (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z)) \to x \underset{˙}{\sim} z$
244	13 3	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
245	244	subm0cl	$⊢ S \in SubMnd ({mulGrp}_{R}) \to \underset{˙}{1} \in S$
246	9 245	syl	$⊢ φ \to \underset{˙}{1} \in S$
247	246	adantr	$⊢ (φ \land x \in W) \to \underset{˙}{1} \in S$
248		oveq1	$⊢ t = \underset{˙}{1} \to t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{1} \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)))$
249	248	eqeq1d	$⊢ t = \underset{˙}{1} \to (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0} \leftrightarrow \underset{˙}{1} \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
250	249	adantl	$⊢ ((φ \land x \in W) \land t = \underset{˙}{1}) \to (t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0} \leftrightarrow \underset{˙}{1} \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
251	40	adantr	$⊢ (φ \land x \in W) \to R \in Ring$
252	46	adantl	$⊢ (φ \land x \in W) \to 1^{st} (x) \in B$
253	16	adantr	$⊢ (φ \land x \in W) \to S \subseteq B$
254	59	adantl	$⊢ (φ \land x \in W) \to 2^{nd} (x) \in S$
255	253 254	sseldd	$⊢ (φ \land x \in W) \to 2^{nd} (x) \in B$
256	1 4 251 252 255	ringcld	$⊢ (φ \land x \in W) \to 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x) \in B$
257	1 2 5	grpsubid	$⊢ (R \in Grp \land 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x) \in B) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) = \underset{˙}{0}$
258	41 256 257	syl2an2r	$⊢ (φ \land x \in W) \to (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) = \underset{˙}{0}$
259	258	oveq2d	$⊢ (φ \land x \in W) \to \underset{˙}{1} \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{1} \underset{˙}{\cdot} \underset{˙}{0}$
260	41 233	syl	$⊢ φ \to \underset{˙}{0} \in B$
261	1 4 3 40 260	ringlidmd	$⊢ φ \to \underset{˙}{1} \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
262	261	adantr	$⊢ (φ \land x \in W) \to \underset{˙}{1} \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
263	259 262	eqtrd	$⊢ (φ \land x \in W) \to \underset{˙}{1} \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
264	247 250 263	rspcedvd	$⊢ (φ \land x \in W) \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}$
265	264	ex	$⊢ φ \to (x \in W \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
266	265	pm4.71d	$⊢ φ \to (x \in W \leftrightarrow (x \in W \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}))$
267		pm4.24	$⊢ x \in W \leftrightarrow (x \in W \land x \in W)$
268	267	anbi1i	$⊢ (x \in W \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}) \leftrightarrow ((x \in W \land x \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
269	266 268	bitrdi	$⊢ φ \to (x \in W \leftrightarrow ((x \in W \land x \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}))$
270		simpl	$⊢ (a = x \land b = x) \to a = x$
271	270	fveq2d	$⊢ (a = x \land b = x) \to 1^{st} (a) = 1^{st} (x)$
272		simpr	$⊢ (a = x \land b = x) \to b = x$
273	272	fveq2d	$⊢ (a = x \land b = x) \to 2^{nd} (b) = 2^{nd} (x)$
274	271 273	oveq12d	$⊢ (a = x \land b = x) \to 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b) = 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)$
275	272	fveq2d	$⊢ (a = x \land b = x) \to 1^{st} (b) = 1^{st} (x)$
276	270	fveq2d	$⊢ (a = x \land b = x) \to 2^{nd} (a) = 2^{nd} (x)$
277	275 276	oveq12d	$⊢ (a = x \land b = x) \to 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a) = 1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)$
278	274 277	oveq12d	$⊢ (a = x \land b = x) \to (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)) = (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))$
279	278	oveq2d	$⊢ (a = x \land b = x) \to t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)))$
280	279	eqeq1d	$⊢ (a = x \land b = x) \to (t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
281	280	rexbidv	$⊢ (a = x \land b = x) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
282	281	adantl	$⊢ (φ \land (a = x \land b = x)) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0})$
283	18 282	brab2d	$⊢ φ \to (x \underset{˙}{\sim} x \leftrightarrow ((x \in W \land x \in W) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x)) \underset{˙}{-} (1^{st} (x) \underset{˙}{\cdot} 2^{nd} (x))) = \underset{˙}{0}))$
284	269 283	bitr4d	$⊢ φ \to (x \in W \leftrightarrow x \underset{˙}{\sim} x)$
285	20 97 243 284	iserd	$⊢ φ \to \underset{˙}{\sim} Er W$

Metamath Proof Explorer

Theorem erler

Proof