Theorem rlocmulval 33710

Description: Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025.)

Hypotheses

Ref	Expression
rlocaddval.1	⊢ 𝐵 = (Base‘𝑅)
rlocaddval.2	⊢ · = (.r‘𝑅)
rlocaddval.3	⊢ + = (+g‘𝑅)
rlocaddval.4	⊢ 𝐿 = (𝑅 RLocal 𝑆)
rlocaddval.5	⊢ ∼ = (𝑅 ~RL 𝑆)
rlocaddval.r	⊢ (𝜑 → 𝑅 ∈ CRing)
rlocaddval.s	⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
rlocaddval.6	⊢ (𝜑 → 𝐸 ∈ 𝐵)
rlocaddval.7	⊢ (𝜑 → 𝐹 ∈ 𝐵)
rlocaddval.8	⊢ (𝜑 → 𝐺 ∈ 𝑆)
rlocaddval.9	⊢ (𝜑 → 𝐻 ∈ 𝑆)
rlocmulval.1	⊢ ⊗ = (.r‘𝐿)

Assertion

Ref	Expression
rlocmulval	⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ )

Proof of Theorem rlocmulval

Dummy variables 𝑝 𝑞 𝑢 𝑣 𝑎 𝑏 𝑘 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rlocaddval.6	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝐵)
2		rlocaddval.8	. . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝑆)
3	1, 2	opelxpd 5694	. . 3 ⊢ (𝜑 → ⟨𝐸, 𝐺⟩ ∈ (𝐵 × 𝑆))
4		rlocaddval.7	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
5		rlocaddval.9	. . . 4 ⊢ (𝜑 → 𝐻 ∈ 𝑆)
6	4, 5	opelxpd 5694	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝐵 × 𝑆))
7		rlocaddval.4	. . . . 5 ⊢ 𝐿 = (𝑅 RLocal 𝑆)
8		rlocaddval.1	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
9		eqid 2760	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
10		rlocaddval.2	. . . . . 6 ⊢ · = (.r‘𝑅)
11		eqid 2760	. . . . . 6 ⊢ (-g‘𝑅) = (-g‘𝑅)
12		rlocaddval.3	. . . . . 6 ⊢ + = (+g‘𝑅)
13		eqid 2760	. . . . . 6 ⊢ (le‘𝑅) = (le‘𝑅)
14		eqid 2760	. . . . . 6 ⊢ (Scalar‘𝑅) = (Scalar‘𝑅)
15		eqid 2760	. . . . . 6 ⊢ (Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅))
16		eqid 2760	. . . . . 6 ⊢ ( ·𝑠 ‘𝑅) = ( ·𝑠 ‘𝑅)
17		eqid 2760	. . . . . 6 ⊢ (𝐵 × 𝑆) = (𝐵 × 𝑆)
18		rlocaddval.5	. . . . . 6 ⊢ ∼ = (𝑅 ~RL 𝑆)
19		eqid 2760	. . . . . 6 ⊢ (TopSet‘𝑅) = (TopSet‘𝑅)
20		eqid 2760	. . . . . 6 ⊢ (dist‘𝑅) = (dist‘𝑅)
21		eqid 2760	. . . . . 6 ⊢ (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
22		eqid 2760	. . . . . 6 ⊢ (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
23		eqid 2760	. . . . . 6 ⊢ (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩) = (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)
24		eqid 2760	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}
25		eqid 2760	. . . . . 6 ⊢ (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))
26		rlocaddval.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CRing)
27		rlocaddval.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
28		eqid 2760	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
29	28, 8	mgpbas 20278	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
30	29	submss 18917	. . . . . . 7 ⊢ (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆 ⊆ 𝐵)
31	27, 30	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
32	8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 31	rlocval 33699	. . . . 5 ⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) /s ∼ ))
33	7, 32	eqtrid 2807	. . . 4 ⊢ (𝜑 → 𝐿 = ((({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) /s ∼ ))
34		eqidd 2761	. . . . . 6 ⊢ (𝜑 → (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) = (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))
35		eqid 2760	. . . . . . 7 ⊢ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) = (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})
36	35	imasvalstr 17536	. . . . . 6 ⊢ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) Struct ⟨1, ;12⟩
37		baseid 17304	. . . . . 6 ⊢ Base = Slot (Base‘ndx)
38		snsstp1 4777	. . . . . . 7 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩} ⊆ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩}
39		ssun1 4124	. . . . . . . 8 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ⊆ ({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩})
40		ssun1 4124	. . . . . . . 8 ⊢ ({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ⊆ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})
41	39, 40	sstri 3940	. . . . . . 7 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ⊆ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})
42	38, 41	sstri 3940	. . . . . 6 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩} ⊆ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})
43	8	fvexi 6892	. . . . . . . 8 ⊢ 𝐵 ∈ V
44	43	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
45	44, 27	xpexd 7750	. . . . . 6 ⊢ (𝜑 → (𝐵 × 𝑆) ∈ V)
46		eqid 2760	. . . . . 6 ⊢ (Base‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})) = (Base‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))
47	34, 36, 37, 42, 45, 46	strfv3 17296	. . . . 5 ⊢ (𝜑 → (Base‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})) = (𝐵 × 𝑆))
48	47	eqcomd 2766	. . . 4 ⊢ (𝜑 → (𝐵 × 𝑆) = (Base‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})))
49		eqid 2760	. . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅)
50	8, 9, 49, 10, 11, 17, 18, 26, 27	erler 33705	. . . 4 ⊢ (𝜑 → ∼ Er (𝐵 × 𝑆))
51		tpex 7747	. . . . . . 7 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∈ V
52		tpex 7747	. . . . . . 7 ⊢ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩} ∈ V
53	51, 52	unex 7746	. . . . . 6 ⊢ ({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∈ V
54		tpex 7747	. . . . . 6 ⊢ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩} ∈ V
55	53, 54	unex 7746	. . . . 5 ⊢ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) ∈ V
56	55	a1i 11	. . . 4 ⊢ (𝜑 → (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}) ∈ V)
57	31	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑆 ⊆ 𝐵)
58	57	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → 𝑆 ⊆ 𝐵)
59	58	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑆 ⊆ 𝐵)
60		eqidd 2761	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
61		eqidd 2761	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
62	26	crngringd 20385	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ Ring)
63	62	ad6antr 749	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑅 ∈ Ring)
64		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑢 ∼ 𝑝)
65	8, 18, 57, 64	erlcl1 33700	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑢 ∈ (𝐵 × 𝑆))
66	65	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑢 ∈ (𝐵 × 𝑆))
67		xp1st 8018	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝐵 × 𝑆) → (1st ‘𝑢) ∈ 𝐵)
68	66, 67	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑢) ∈ 𝐵)
69		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑣 ∼ 𝑞)
70	8, 18, 57, 69	erlcl1 33700	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑣 ∈ (𝐵 × 𝑆))
71	70	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑣 ∈ (𝐵 × 𝑆))
72		xp1st 8018	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐵 × 𝑆) → (1st ‘𝑣) ∈ 𝐵)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑣) ∈ 𝐵)
74	8, 10, 63, 68, 73	ringcld 20396	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑢) · (1st ‘𝑣)) ∈ 𝐵)
75	8, 18, 57, 64	erlcl2 33701	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑝 ∈ (𝐵 × 𝑆))
76	75	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑝 ∈ (𝐵 × 𝑆))
77		xp1st 8018	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝐵 × 𝑆) → (1st ‘𝑝) ∈ 𝐵)
78	76, 77	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑝) ∈ 𝐵)
79	8, 18, 57, 69	erlcl2 33701	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑞 ∈ (𝐵 × 𝑆))
80	79	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑞 ∈ (𝐵 × 𝑆))
81		xp1st 8018	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ (𝐵 × 𝑆) → (1st ‘𝑞) ∈ 𝐵)
82	80, 81	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑞) ∈ 𝐵)
83	8, 10, 63, 78, 82	ringcld 20396	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (1st ‘𝑞)) ∈ 𝐵)
84	27	ad6antr 749	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
85		xp2nd 8019	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝐵 × 𝑆) → (2nd ‘𝑢) ∈ 𝑆)
86	66, 85	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑢) ∈ 𝑆)
87		xp2nd 8019	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐵 × 𝑆) → (2nd ‘𝑣) ∈ 𝑆)
88	71, 87	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑣) ∈ 𝑆)
89	28, 10	mgpplusg 20277	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
90	89	submcl 18920	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (2nd ‘𝑢) ∈ 𝑆 ∧ (2nd ‘𝑣) ∈ 𝑆) → ((2nd ‘𝑢) · (2nd ‘𝑣)) ∈ 𝑆)
91	84, 86, 88, 90	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑢) · (2nd ‘𝑣)) ∈ 𝑆)
92		xp2nd 8019	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝐵 × 𝑆) → (2nd ‘𝑝) ∈ 𝑆)
93	76, 92	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑝) ∈ 𝑆)
94		xp2nd 8019	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ (𝐵 × 𝑆) → (2nd ‘𝑞) ∈ 𝑆)
95	80, 94	syl 18	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑞) ∈ 𝑆)
96	89	submcl 18920	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (2nd ‘𝑝) ∈ 𝑆 ∧ (2nd ‘𝑞) ∈ 𝑆) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝑆)
97	84, 93, 95, 96	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝑆)
98		simp-4r 796	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑓 ∈ 𝑆)
99		simplr 781	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑔 ∈ 𝑆)
100	89	submcl 18920	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) → (𝑓 · 𝑔) ∈ 𝑆)
101	84, 98, 99, 100	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · 𝑔) ∈ 𝑆)
102	59, 101	sseldd 3932	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · 𝑔) ∈ 𝐵)
103	59, 97	sseldd 3932	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝐵)
104	8, 10, 63, 74, 103	ringcld 20396	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))) ∈ 𝐵)
105	59, 91	sseldd 3932	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑢) · (2nd ‘𝑣)) ∈ 𝐵)
106	8, 10, 63, 83, 105	ringcld 20396	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))) ∈ 𝐵)
107	8, 10, 11, 63, 102, 104, 106	ringsubdi 20449	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · ((((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞)))(-g‘𝑅)(((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))) = (((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))))
108	63	ringgrpd 20381	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑅 ∈ Grp)
109	8, 10, 63, 102, 104	ringcld 20396	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞)))) ∈ 𝐵)
110	8, 10, 63, 78, 73	ringcld 20396	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (1st ‘𝑣)) ∈ 𝐵)
111	59, 86	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑢) ∈ 𝐵)
112	59, 95	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑞) ∈ 𝐵)
113	8, 10, 63, 111, 112	ringcld 20396	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑢) · (2nd ‘𝑞)) ∈ 𝐵)
114	8, 10, 63, 110, 113	ringcld 20396	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))) ∈ 𝐵)
115	8, 10, 63, 102, 114	ringcld 20396	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) ∈ 𝐵)
116	8, 10, 63, 102, 106	ringcld 20396	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))) ∈ 𝐵)
117	8, 12, 11	grpnpncan 19158	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Grp ∧ (((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞)))) ∈ 𝐵 ∧ ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) ∈ 𝐵 ∧ ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))) ∈ 𝐵)) → ((((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))) + (((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))))) = (((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))))
118	108, 109, 115, 116, 117	syl13anc 1399	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))) + (((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))))) = (((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))))
119	26	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑅 ∈ CRing)
120	119	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → 𝑅 ∈ CRing)
121	120	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑅 ∈ CRing)
122	28	crngmgp 20380	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
123	121, 122	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (mulGrp‘𝑅) ∈ CMnd)
124	59, 98	sseldd 3932	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑓 ∈ 𝐵)
125	59, 99	sseldd 3932	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑔 ∈ 𝐵)
126	59, 93	sseldd 3932	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑝) ∈ 𝐵)
127	29, 89, 123, 124, 125, 68, 73, 126, 112	cmn246135 33473	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞)))) = ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))))
128	29, 89, 123, 124, 125, 78, 73, 111, 112	cmn246135 33473	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) = ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢)))))
129	127, 128	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))) = (((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝))))(-g‘𝑅)((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))))))
130	8, 10, 63, 73, 112	ringcld 20396	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑣) · (2nd ‘𝑞)) ∈ 𝐵)
131	8, 10, 63, 125, 130	ringcld 20396	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) ∈ 𝐵)
132	8, 10, 63, 68, 126	ringcld 20396	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑢) · (2nd ‘𝑝)) ∈ 𝐵)
133	8, 10, 63, 124, 132	ringcld 20396	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝))) ∈ 𝐵)
134	8, 10, 63, 78, 111	ringcld 20396	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (2nd ‘𝑢)) ∈ 𝐵)
135	8, 10, 63, 124, 134	ringcld 20396	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) ∈ 𝐵)
136	8, 10, 11, 63, 131, 133, 135	ringsubdi 20449	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · ((𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))(-g‘𝑅)(𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))))) = (((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝))))(-g‘𝑅)((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))))))
137	8, 10, 11, 63, 124, 132, 134	ringsubdi 20449	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = ((𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))(-g‘𝑅)(𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢)))))
138		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅))
139	137, 138	eqtr3d 2797	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))(-g‘𝑅)(𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅))
140	139	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · ((𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))(-g‘𝑅)(𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))))) = ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (0g‘𝑅)))
141	8, 10, 9, 63, 131	ringrzd 20438	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (0g‘𝑅)) = (0g‘𝑅))
142	140, 141	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · ((𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))(-g‘𝑅)(𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))))) = (0g‘𝑅))
143	136, 142	eqtr3d 2797	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝))))(-g‘𝑅)((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))))) = (0g‘𝑅))
144	129, 143	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))) = (0g‘𝑅))
145	8, 10, 121, 78, 73	crngcomd 20394	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (1st ‘𝑣)) = ((1st ‘𝑣) · (1st ‘𝑝)))
146	145	oveq1d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))) = (((1st ‘𝑣) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))
147	146	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) = ((𝑓 · 𝑔) · (((1st ‘𝑣) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))))
148	29, 89, 123, 124, 125, 73, 78, 111, 112	cmn145236 33474	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑣) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) = ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))))
149	147, 148	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) = ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))))
150	8, 10, 121, 82, 78	crngcomd 20394	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑞) · (1st ‘𝑝)) = ((1st ‘𝑝) · (1st ‘𝑞)))
151	150	oveq1d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑞) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑣))) = (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))
152	151	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑞) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))) = ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))))
153	59, 88	sseldd 3932	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑣) ∈ 𝐵)
154	29, 89, 123, 124, 125, 82, 78, 111, 153	cmn145236 33474	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑞) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))) = ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣)))))
155	152, 154	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))) = ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣)))))
156	149, 155	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))) = (((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))))))
157	8, 10, 63, 82, 153	ringcld 20396	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑞) · (2nd ‘𝑣)) ∈ 𝐵)
158	8, 10, 11, 63, 125, 130, 157	ringsubdi 20449	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))(-g‘𝑅)(𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣)))))
159		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅))
160	158, 159	eqtr3d 2797	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))(-g‘𝑅)(𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅))
161	160	oveq2d 7429	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))(-g‘𝑅)(𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))))) = ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (0g‘𝑅)))
162	8, 10, 63, 125, 157	ringcld 20396	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))) ∈ 𝐵)
163	8, 10, 11, 63, 135, 131, 162	ringsubdi 20449	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))(-g‘𝑅)(𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))))) = (((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))))))
164	8, 10, 9, 63, 135	ringrzd 20438	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (0g‘𝑅)) = (0g‘𝑅))
165	161, 163, 164	3eqtr3d 2803	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))))) = (0g‘𝑅))
166	156, 165	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))) = (0g‘𝑅))
167	144, 166	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))) + (((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))))) = ((0g‘𝑅) + (0g‘𝑅)))
168	8, 9	grpidcl 19089	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Grp → (0g‘𝑅) ∈ 𝐵)
169	108, 168	syl 18	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (0g‘𝑅) ∈ 𝐵)
170	8, 12, 9, 108, 169	grplidd 19093	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((0g‘𝑅) + (0g‘𝑅)) = (0g‘𝑅))
171	167, 170	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))) + (((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))(-g‘𝑅)((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))))) = (0g‘𝑅))
172	107, 118, 171	3eqtr2d 2801	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · ((((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞)))(-g‘𝑅)(((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))) = (0g‘𝑅))
173	8, 18, 59, 9, 10, 11, 60, 61, 74, 83, 91, 97, 101, 172	erlbrd 33703	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
174	69	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → 𝑣 ∼ 𝑞)
175	8, 18, 58, 9, 10, 11, 174	erldi 33702	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → ∃𝑔 ∈ 𝑆 (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅))
176	173, 175	r19.29a 3170	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
177	8, 18, 57, 9, 10, 11, 64	erldi 33702	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ∃𝑓 ∈ 𝑆 (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅))
178	176, 177	r19.29a 3170	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
179		mulridx 17380	. . . . . . . . . . . 12 ⊢ .r = Slot (.r‘ndx)
180		snsstp3 4779	. . . . . . . . . . . . 13 ⊢ {⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ⊆ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩}
181	180, 41	sstri 3940	. . . . . . . . . . . 12 ⊢ {⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ⊆ (({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})
182	22	mpoexg 8075	. . . . . . . . . . . . 13 ⊢ (((𝐵 × 𝑆) ∈ V ∧ (𝐵 × 𝑆) ∈ V) → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) ∈ V)
183	45, 45, 182	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) ∈ V)
184		eqid 2760	. . . . . . . . . . . 12 ⊢ (.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})) = (.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))
185	34, 36, 179, 181, 183, 184	strfv3 17296	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩))
186	185	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩})) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩))
187	186	oveqd 7430	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑢(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑣) = (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑣))
188		opex 5439	. . . . . . . . . . 11 ⊢ ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∈ V
189	188	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∈ V)
190		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢)
191	190	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (1st ‘𝑎) = (1st ‘𝑢))
192		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣)
193	192	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (1st ‘𝑏) = (1st ‘𝑣))
194	191, 193	oveq12d 7431	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((1st ‘𝑎) · (1st ‘𝑏)) = ((1st ‘𝑢) · (1st ‘𝑣)))
195	190	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (2nd ‘𝑎) = (2nd ‘𝑢))
196	192	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (2nd ‘𝑏) = (2nd ‘𝑣))
197	195, 196	oveq12d 7431	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((2nd ‘𝑎) · (2nd ‘𝑏)) = ((2nd ‘𝑢) · (2nd ‘𝑣)))
198	194, 197	opeq12d 4841	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩ = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
199	198, 22	ovmpoga 7567	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (𝐵 × 𝑆) ∧ 𝑣 ∈ (𝐵 × 𝑆) ∧ ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∈ V) → (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑣) = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
200	65, 70, 189, 199	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑣) = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
201	187, 200	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑢(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑣) = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
202	186	oveqd 7430	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) = (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞))
203		opex 5439	. . . . . . . . . . 11 ⊢ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V
204	203	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V)
205		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → 𝑎 = 𝑝)
206	205	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (1st ‘𝑎) = (1st ‘𝑝))
207		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → 𝑏 = 𝑞)
208	207	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (1st ‘𝑏) = (1st ‘𝑞))
209	206, 208	oveq12d 7431	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → ((1st ‘𝑎) · (1st ‘𝑏)) = ((1st ‘𝑝) · (1st ‘𝑞)))
210	205	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (2nd ‘𝑎) = (2nd ‘𝑝))
211	207	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (2nd ‘𝑏) = (2nd ‘𝑞))
212	210, 211	oveq12d 7431	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → ((2nd ‘𝑎) · (2nd ‘𝑏)) = ((2nd ‘𝑝) · (2nd ‘𝑞)))
213	209, 212	opeq12d 4841	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩ = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
214	213, 22	ovmpoga 7567	. . . . . . . . . 10 ⊢ ((𝑝 ∈ (𝐵 × 𝑆) ∧ 𝑞 ∈ (𝐵 × 𝑆) ∧ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
215	75, 79, 204, 214	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
216	202, 215	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
217	201, 216	breq12d 5116	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ((𝑢(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑣) ∼ (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) ↔ ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩))
218	178, 217	mpbird 260	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑢(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑣) ∼ (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞))
219	218	anasss 472	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∼ 𝑝 ∧ 𝑣 ∼ 𝑞)) → (𝑢(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑣) ∼ (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞))
220	219	ex 418	. . . 4 ⊢ (𝜑 → ((𝑢 ∼ 𝑝 ∧ 𝑣 ∼ 𝑞) → (𝑢(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑣) ∼ (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞)))
221	185	oveqd 7430	. . . . . . 7 ⊢ (𝜑 → (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) = (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞))
222	221	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) = (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞))
223		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑝 ∈ (𝐵 × 𝑆))
224		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑞 ∈ (𝐵 × 𝑆))
225	203	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V)
226	223, 224, 225, 214	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
227	62	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑅 ∈ Ring)
228	223, 77	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (1st ‘𝑝) ∈ 𝐵)
229	224, 81	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (1st ‘𝑞) ∈ 𝐵)
230	8, 10, 227, 228, 229	ringcld 20396	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ((1st ‘𝑝) · (1st ‘𝑞)) ∈ 𝐵)
231	27	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
232	223, 92	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (2nd ‘𝑝) ∈ 𝑆)
233	224, 94	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (2nd ‘𝑞) ∈ 𝑆)
234	231, 232, 233, 96	syl3anc 1398	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝑆)
235	230, 234	opelxpd 5694	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ (𝐵 × 𝑆))
236	226, 235	eqeltrd 2860	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) ∈ (𝐵 × 𝑆))
237	222, 236	eqeltrd 2860	. . . . 5 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) ∈ (𝐵 × 𝑆))
238	237	anasss 472	. . . 4 ⊢ ((𝜑 ∧ (𝑝 ∈ (𝐵 × 𝑆) ∧ 𝑞 ∈ (𝐵 × 𝑆))) → (𝑝(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))𝑞) ∈ (𝐵 × 𝑆))
239		rlocmulval.1	. . . 4 ⊢ ⊗ = (.r‘𝐿)
240	33, 48, 50, 56, 220, 238, 184, 239	qusmulval 17641	. . 3 ⊢ ((𝜑 ∧ ⟨𝐸, 𝐺⟩ ∈ (𝐵 × 𝑆) ∧ ⟨𝐹, 𝐻⟩ ∈ (𝐵 × 𝑆)) → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [(⟨𝐸, 𝐺⟩(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))⟨𝐹, 𝐻⟩)] ∼ )
241	3, 6, 240	mpd3an23 1492	. 2 ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [(⟨𝐸, 𝐺⟩(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))⟨𝐹, 𝐻⟩)] ∼ )
242	185	oveqd 7430	. . . 4 ⊢ (𝜑 → (⟨𝐸, 𝐺⟩(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))⟨𝐹, 𝐻⟩) = (⟨𝐸, 𝐺⟩(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟨𝐹, 𝐻⟩))
243	22	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩))
244		simprl 783	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝑎 = ⟨𝐸, 𝐺⟩)
245	244	fveq2d 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑎) = (1st ‘⟨𝐸, 𝐺⟩))
246	1	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐸 ∈ 𝐵)
247	2	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐺 ∈ 𝑆)
248		op1stg 7998	. . . . . . . . 9 ⊢ ((𝐸 ∈ 𝐵 ∧ 𝐺 ∈ 𝑆) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
249	246, 247, 248	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
250	245, 249	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑎) = 𝐸)
251		simprr 785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝑏 = ⟨𝐹, 𝐻⟩)
252	251	fveq2d 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑏) = (1st ‘⟨𝐹, 𝐻⟩))
253	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐹 ∈ 𝐵)
254	5	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐻 ∈ 𝑆)
255		op1stg 7998	. . . . . . . . 9 ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐻 ∈ 𝑆) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
256	253, 254, 255	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
257	252, 256	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑏) = 𝐹)
258	250, 257	oveq12d 7431	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ((1st ‘𝑎) · (1st ‘𝑏)) = (𝐸 · 𝐹))
259	244	fveq2d 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑎) = (2nd ‘⟨𝐸, 𝐺⟩))
260		op2ndg 7999	. . . . . . . . 9 ⊢ ((𝐸 ∈ 𝐵 ∧ 𝐺 ∈ 𝑆) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
261	246, 247, 260	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
262	259, 261	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑎) = 𝐺)
263	251	fveq2d 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑏) = (2nd ‘⟨𝐹, 𝐻⟩))
264		op2ndg 7999	. . . . . . . . 9 ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐻 ∈ 𝑆) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
265	253, 254, 264	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
266	263, 265	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑏) = 𝐻)
267	262, 266	oveq12d 7431	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ((2nd ‘𝑎) · (2nd ‘𝑏)) = (𝐺 · 𝐻))
268	258, 267	opeq12d 4841	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩ = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
269		opex 5439	. . . . . 6 ⊢ ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩ ∈ V
270	269	a1i 11	. . . . 5 ⊢ (𝜑 → ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩ ∈ V)
271	243, 268, 3, 6, 270	ovmpod 7565	. . . 4 ⊢ (𝜑 → (⟨𝐸, 𝐺⟩(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟨𝐹, 𝐻⟩) = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
272	242, 271	eqtrd 2795	. . 3 ⊢ (𝜑 → (⟨𝐸, 𝐺⟩(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))⟨𝐹, 𝐻⟩) = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
273	272	eceq1d 8737	. 2 ⊢ (𝜑 → [(⟨𝐸, 𝐺⟩(.r‘(({⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))⟩}))⟨𝐹, 𝐻⟩)] ∼ = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ )
274	241, 273	eqtrd 2795	1 ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ )

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279  {csn 4584  {ctp 4588  ⟨cop 4590   class class class wbr 5103  {copab 5167   × cxp 5653  ‘cfv 6533  (class class class)co 7413   ∈ cmpo 7415  1^st c1st 7984  2^nd c2nd 7985  [cec 8694  1c1 11125  2c2 12319  ;cdc 12736  ndxcnx 17285  Basecbs 17301  +_gcplusg 17342  ._rcmulr 17343  Scalarcsca 17345   ·_𝑠 cvsca 17346  ·_𝑖cip 17347  TopSetcts 17348  lecple 17349  distcds 17351   ↾_t crest 17505  0_gc0g 17524   /_s cqus 17591  SubMndcsubmnd 18890  Grpcgrp 19057  -_gcsg 19059  CMndccmn 19907  mulGrpcmgp 20273  1_rcur 20320  Ringcrg 20372  CRingccrg 20373   ×_t ctx 23786   ~_RL cerl 33693   RLocal crloc 33694

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-ec 8698  df-qs 8702  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-inf 9413  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-z 12616  df-dec 12737  df-uz 12888  df-fz 13562  df-struct 17239  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-ress 17323  df-plusg 17355  df-mulr 17356  df-sca 17358  df-vsca 17359  df-ip 17360  df-tset 17361  df-ple 17362  df-ds 17364  df-0g 17526  df-imas 17594  df-qus 17595  df-mgm 18730  df-sgrp 18821  df-mnd 18837  df-submnd 18892  df-grp 19060  df-minusg 19061  df-sbg 19062  df-cmn 19909  df-abl 19910  df-mgp 20274  df-rng 20288  df-ur 20321  df-ring 20374  df-cring 20375  df-erl 33695  df-rloc 33696

This theorem is used by:  rloccring  33711  rloc1r  33713  rlocf1  33714  rlocinvunit  33715  rlocisunit  33716  fracfld  33749  zringfrac  33964