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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	erler.2	⊢ 0 = ( 0_g ‘ 𝑅 )
	erler.3	⊢ 1 = ( 1_r ‘ 𝑅 )
	erler.4	⊢ · = ( ._r ‘ 𝑅 )
	erler.5	⊢ − = ( -_g ‘ 𝑅 )
	erler.w	⊢ 𝑊 = ( 𝐵 × 𝑆 )
	erler.q	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	erler.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	erler.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
Assertion	erler	⊢ ( 𝜑 → ∼ Er 𝑊 )

Proof

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

Metamath Proof Explorer

Theorem erler

Proof