Theorem rlocmulval 33227

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 5680	. . 3 ⊢ (𝜑 → ⟨𝐸, 𝐺⟩ ∈ (𝐵 × 𝑆))
4		rlocaddval.7	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
5		rlocaddval.9	. . . 4 ⊢ (𝜑 → 𝐻 ∈ 𝑆)
6	4, 5	opelxpd 5680	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝐵 × 𝑆))
7		rlocaddval.4	. . . . 5 ⊢ 𝐿 = (𝑅 RLocal 𝑆)
8		rlocaddval.1	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
9		eqid 2730	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
10		rlocaddval.2	. . . . . 6 ⊢ · = (.r‘𝑅)
11		eqid 2730	. . . . . 6 ⊢ (-g‘𝑅) = (-g‘𝑅)
12		rlocaddval.3	. . . . . 6 ⊢ + = (+g‘𝑅)
13		eqid 2730	. . . . . 6 ⊢ (le‘𝑅) = (le‘𝑅)
14		eqid 2730	. . . . . 6 ⊢ (Scalar‘𝑅) = (Scalar‘𝑅)
15		eqid 2730	. . . . . 6 ⊢ (Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅))
16		eqid 2730	. . . . . 6 ⊢ ( ·𝑠 ‘𝑅) = ( ·𝑠 ‘𝑅)
17		eqid 2730	. . . . . 6 ⊢ (𝐵 × 𝑆) = (𝐵 × 𝑆)
18		rlocaddval.5	. . . . . 6 ⊢ ∼ = (𝑅 ~RL 𝑆)
19		eqid 2730	. . . . . 6 ⊢ (TopSet‘𝑅) = (TopSet‘𝑅)
20		eqid 2730	. . . . . 6 ⊢ (dist‘𝑅) = (dist‘𝑅)
21		eqid 2730	. . . . . 6 ⊢ (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
22		eqid 2730	. . . . . 6 ⊢ (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)
23		eqid 2730	. . . . . 6 ⊢ (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩) = (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)
24		eqid 2730	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st ‘𝑎) · (2nd ‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))}
25		eqid 2730	. . . . . 6 ⊢ (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎)))) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st ‘𝑎) · (2nd ‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd ‘𝑎))))
26		rlocaddval.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CRing)
27		rlocaddval.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
28		eqid 2730	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
29	28, 8	mgpbas 20061	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
30	29	submss 18743	. . . . . . 7 ⊢ (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆 ⊆ 𝐵)
31	27, 30	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
32	8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 31	rlocval 33217	. . . . 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 2777	. . . 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 2731	. . . . . 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 2730	. . . . . . 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 17421	. . . . . 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 17189	. . . . . 6 ⊢ Base = Slot (Base‘ndx)
38		snsstp1 4783	. . . . . . 7 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩} ⊆ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩}
39		ssun1 4144	. . . . . . . 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 4144	. . . . . . . 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 3959	. . . . . . 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 3959	. . . . . 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 6875	. . . . . . . 8 ⊢ 𝐵 ∈ V
44	43	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
45	44, 27	xpexd 7730	. . . . . 6 ⊢ (𝜑 → (𝐵 × 𝑆) ∈ V)
46		eqid 2730	. . . . . 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 17181	. . . . 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 2736	. . . 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 2730	. . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅)
50	8, 9, 49, 10, 11, 17, 18, 26, 27	erler 33223	. . . 4 ⊢ (𝜑 → ∼ Er (𝐵 × 𝑆))
51		tpex 7725	. . . . . . 7 ⊢ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st ‘𝑎) · (2nd ‘𝑏)) + ((1st ‘𝑏) · (2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟩} ∈ V
52		tpex 7725	. . . . . . 7 ⊢ {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠 ‘𝑅)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩} ∈ V
53	51, 52	unex 7723	. . . . . 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 7725	. . . . . 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 7723	. . . . 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 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑆 ⊆ 𝐵)
58	57	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → 𝑆 ⊆ 𝐵)
59	58	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑆 ⊆ 𝐵)
60		eqidd 2731	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
61		eqidd 2731	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
62	26	crngringd 20162	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ Ring)
63	62	ad6antr 736	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑅 ∈ Ring)
64		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑢 ∼ 𝑝)
65	8, 18, 57, 64	erlcl1 33218	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑢 ∈ (𝐵 × 𝑆))
66	65	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑢 ∈ (𝐵 × 𝑆))
67		xp1st 8003	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝐵 × 𝑆) → (1st ‘𝑢) ∈ 𝐵)
68	66, 67	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑢) ∈ 𝐵)
69		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑣 ∼ 𝑞)
70	8, 18, 57, 69	erlcl1 33218	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑣 ∈ (𝐵 × 𝑆))
71	70	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑣 ∈ (𝐵 × 𝑆))
72		xp1st 8003	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐵 × 𝑆) → (1st ‘𝑣) ∈ 𝐵)
73	71, 72	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑣) ∈ 𝐵)
74	8, 10, 63, 68, 73	ringcld 20176	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑢) · (1st ‘𝑣)) ∈ 𝐵)
75	8, 18, 57, 64	erlcl2 33219	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑝 ∈ (𝐵 × 𝑆))
76	75	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑝 ∈ (𝐵 × 𝑆))
77		xp1st 8003	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝐵 × 𝑆) → (1st ‘𝑝) ∈ 𝐵)
78	76, 77	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑝) ∈ 𝐵)
79	8, 18, 57, 69	erlcl2 33219	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑞 ∈ (𝐵 × 𝑆))
80	79	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑞 ∈ (𝐵 × 𝑆))
81		xp1st 8003	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ (𝐵 × 𝑆) → (1st ‘𝑞) ∈ 𝐵)
82	80, 81	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (1st ‘𝑞) ∈ 𝐵)
83	8, 10, 63, 78, 82	ringcld 20176	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (1st ‘𝑞)) ∈ 𝐵)
84	27	ad6antr 736	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
85		xp2nd 8004	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝐵 × 𝑆) → (2nd ‘𝑢) ∈ 𝑆)
86	66, 85	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑢) ∈ 𝑆)
87		xp2nd 8004	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐵 × 𝑆) → (2nd ‘𝑣) ∈ 𝑆)
88	71, 87	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑣) ∈ 𝑆)
89	28, 10	mgpplusg 20060	. . . . . . . . . . . 12 ⊢ · = (+g‘(mulGrp‘𝑅))
90	89	submcl 18746	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (2nd ‘𝑢) ∈ 𝑆 ∧ (2nd ‘𝑣) ∈ 𝑆) → ((2nd ‘𝑢) · (2nd ‘𝑣)) ∈ 𝑆)
91	84, 86, 88, 90	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑢) · (2nd ‘𝑣)) ∈ 𝑆)
92		xp2nd 8004	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝐵 × 𝑆) → (2nd ‘𝑝) ∈ 𝑆)
93	76, 92	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑝) ∈ 𝑆)
94		xp2nd 8004	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ (𝐵 × 𝑆) → (2nd ‘𝑞) ∈ 𝑆)
95	80, 94	syl 17	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑞) ∈ 𝑆)
96	89	submcl 18746	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (2nd ‘𝑝) ∈ 𝑆 ∧ (2nd ‘𝑞) ∈ 𝑆) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝑆)
97	84, 93, 95, 96	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝑆)
98		simp-4r 783	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑓 ∈ 𝑆)
99		simplr 768	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑔 ∈ 𝑆)
100	89	submcl 18746	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) → (𝑓 · 𝑔) ∈ 𝑆)
101	84, 98, 99, 100	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · 𝑔) ∈ 𝑆)
102	59, 101	sseldd 3950	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · 𝑔) ∈ 𝐵)
103	59, 97	sseldd 3950	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝐵)
104	8, 10, 63, 74, 103	ringcld 20176	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞))) ∈ 𝐵)
105	59, 91	sseldd 3950	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑢) · (2nd ‘𝑣)) ∈ 𝐵)
106	8, 10, 63, 83, 105	ringcld 20176	. . . . . . . . . . . 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 20223	. . . . . . . . . . 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 20158	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑅 ∈ Grp)
109	8, 10, 63, 102, 104	ringcld 20176	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑢) · (1st ‘𝑣)) · ((2nd ‘𝑝) · (2nd ‘𝑞)))) ∈ 𝐵)
110	8, 10, 63, 78, 73	ringcld 20176	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (1st ‘𝑣)) ∈ 𝐵)
111	59, 86	sseldd 3950	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑢) ∈ 𝐵)
112	59, 95	sseldd 3950	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (2nd ‘𝑞) ∈ 𝐵)
113	8, 10, 63, 111, 112	ringcld 20176	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((2nd ‘𝑢) · (2nd ‘𝑞)) ∈ 𝐵)
114	8, 10, 63, 110, 113	ringcld 20176	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))) ∈ 𝐵)
115	8, 10, 63, 102, 114	ringcld 20176	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞)))) ∈ 𝐵)
116	8, 10, 63, 102, 106	ringcld 20176	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · 𝑔) · (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣)))) ∈ 𝐵)
117	8, 12, 11	grpnpncan 18974	. . . . . . . . . . . 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 1374	. . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → 𝑅 ∈ CRing)
120	119	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → 𝑅 ∈ CRing)
121	120	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑅 ∈ CRing)
122	28	crngmgp 20157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
123	121, 122	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (mulGrp‘𝑅) ∈ CMnd)
124	59, 98	sseldd 3950	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑓 ∈ 𝐵)
125	59, 99	sseldd 3950	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → 𝑔 ∈ 𝐵)
126	59, 93	sseldd 3950	. . . . . . . . . . . . . . . 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 32981	. . . . . . . . . . . . . . 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 32981	. . . . . . . . . . . . . . 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 7408	. . . . . . . . . . . . . 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 20176	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑣) · (2nd ‘𝑞)) ∈ 𝐵)
131	8, 10, 63, 125, 130	ringcld 20176	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) ∈ 𝐵)
132	8, 10, 63, 68, 126	ringcld 20176	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑢) · (2nd ‘𝑝)) ∈ 𝐵)
133	8, 10, 63, 124, 132	ringcld 20176	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝))) ∈ 𝐵)
134	8, 10, 63, 78, 111	ringcld 20176	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (2nd ‘𝑢)) ∈ 𝐵)
135	8, 10, 63, 124, 134	ringcld 20176	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) ∈ 𝐵)
136	8, 10, 11, 63, 131, 133, 135	ringsubdi 20223	. . . . . . . . . . . . . . 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 20223	. . . . . . . . . . . . . . . . . 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 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅))
139	137, 138	eqtr3d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · ((1st ‘𝑢) · (2nd ‘𝑝)))(-g‘𝑅)(𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅))
140	139	oveq2d 7406	. . . . . . . . . . . . . . . 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 20212	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞))) · (0g‘𝑅)) = (0g‘𝑅))
142	140, 141	eqtrd 2765	. . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . 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 20171	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑝) · (1st ‘𝑣)) = ((1st ‘𝑣) · (1st ‘𝑝)))
146	145	oveq1d 7405	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑝) · (1st ‘𝑣)) · ((2nd ‘𝑢) · (2nd ‘𝑞))) = (((1st ‘𝑣) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑞))))
147	146	oveq2d 7406	. . . . . . . . . . . . . . . 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 32982	. . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . 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 20171	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑞) · (1st ‘𝑝)) = ((1st ‘𝑝) · (1st ‘𝑞)))
151	150	oveq1d 7405	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (((1st ‘𝑞) · (1st ‘𝑝)) · ((2nd ‘𝑢) · (2nd ‘𝑣))) = (((1st ‘𝑝) · (1st ‘𝑞)) · ((2nd ‘𝑢) · (2nd ‘𝑣))))
152	151	oveq2d 7406	. . . . . . . . . . . . . . . 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 3950	. . . . . . . . . . . . . . . . 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 32982	. . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . 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 7408	. . . . . . . . . . . . . 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 20176	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((1st ‘𝑞) · (2nd ‘𝑣)) ∈ 𝐵)
158	8, 10, 11, 63, 125, 130, 157	ringsubdi 20223	. . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅))
160	158, 159	eqtr3d 2767	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑔 · ((1st ‘𝑣) · (2nd ‘𝑞)))(-g‘𝑅)(𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅))
161	160	oveq2d 7406	. . . . . . . . . . . . . . 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 20176	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (𝑔 · ((1st ‘𝑞) · (2nd ‘𝑣))) ∈ 𝐵)
163	8, 10, 11, 63, 135, 131, 162	ringsubdi 20223	. . . . . . . . . . . . . . 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 20212	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((𝑓 · ((1st ‘𝑝) · (2nd ‘𝑢))) · (0g‘𝑅)) = (0g‘𝑅))
165	161, 163, 164	3eqtr3d 2773	. . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . 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 7408	. . . . . . . . . . . 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 18904	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Grp → (0g‘𝑅) ∈ 𝐵)
169	108, 168	syl 17	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → (0g‘𝑅) ∈ 𝐵)
170	8, 12, 9, 108, 169	grplidd 18908	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ((0g‘𝑅) + (0g‘𝑅)) = (0g‘𝑅))
171	167, 170	eqtrd 2765	. . . . . . . . . . 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 2771	. . . . . . . . . 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 33221	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) ∧ 𝑔 ∈ 𝑆) ∧ (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅)) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
174	69	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → 𝑣 ∼ 𝑞)
175	8, 18, 58, 9, 10, 11, 174	erldi 33220	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → ∃𝑔 ∈ 𝑆 (𝑔 · (((1st ‘𝑣) · (2nd ‘𝑞))(-g‘𝑅)((1st ‘𝑞) · (2nd ‘𝑣)))) = (0g‘𝑅))
176	173, 175	r19.29a 3142	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) ∧ 𝑓 ∈ 𝑆) ∧ (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅)) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
177	8, 18, 57, 9, 10, 11, 64	erldi 33220	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ∃𝑓 ∈ 𝑆 (𝑓 · (((1st ‘𝑢) · (2nd ‘𝑝))(-g‘𝑅)((1st ‘𝑝) · (2nd ‘𝑢)))) = (0g‘𝑅))
178	176, 177	r19.29a 3142	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∼ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
179		mulridx 17265	. . . . . . . . . . . 12 ⊢ .r = Slot (.r‘ndx)
180		snsstp3 4785	. . . . . . . . . . . . 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 3959	. . . . . . . . . . . 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 8058	. . . . . . . . . . . . 13 ⊢ (((𝐵 × 𝑆) ∈ V ∧ (𝐵 × 𝑆) ∈ V) → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) ∈ V)
183	45, 45, 182	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩) ∈ V)
184		eqid 2730	. . . . . . . . . . . 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 17181	. . . . . . . . . . 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 726	. . . . . . . . . 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 7407	. . . . . . . . 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 5427	. . . . . . . . . . 11 ⊢ ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∈ V
189	188	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∈ V)
190		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢)
191	190	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (1st ‘𝑎) = (1st ‘𝑢))
192		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣)
193	192	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (1st ‘𝑏) = (1st ‘𝑣))
194	191, 193	oveq12d 7408	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((1st ‘𝑎) · (1st ‘𝑏)) = ((1st ‘𝑢) · (1st ‘𝑣)))
195	190	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (2nd ‘𝑎) = (2nd ‘𝑢))
196	192	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (2nd ‘𝑏) = (2nd ‘𝑣))
197	195, 196	oveq12d 7408	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((2nd ‘𝑎) · (2nd ‘𝑏)) = ((2nd ‘𝑢) · (2nd ‘𝑣)))
198	194, 197	opeq12d 4848	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩ = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
199	198, 22	ovmpoga 7546	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (𝐵 × 𝑆) ∧ 𝑣 ∈ (𝐵 × 𝑆) ∧ ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩ ∈ V) → (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑣) = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
200	65, 70, 189, 199	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑣) = ⟨((1st ‘𝑢) · (1st ‘𝑣)), ((2nd ‘𝑢) · (2nd ‘𝑣))⟩)
201	187, 200	eqtrd 2765	. . . . . . . 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 7407	. . . . . . . . 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 5427	. . . . . . . . . . 11 ⊢ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V
204	203	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V)
205		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → 𝑎 = 𝑝)
206	205	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (1st ‘𝑎) = (1st ‘𝑝))
207		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → 𝑏 = 𝑞)
208	207	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (1st ‘𝑏) = (1st ‘𝑞))
209	206, 208	oveq12d 7408	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → ((1st ‘𝑎) · (1st ‘𝑏)) = ((1st ‘𝑝) · (1st ‘𝑞)))
210	205	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (2nd ‘𝑎) = (2nd ‘𝑝))
211	207	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → (2nd ‘𝑏) = (2nd ‘𝑞))
212	210, 211	oveq12d 7408	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → ((2nd ‘𝑎) · (2nd ‘𝑏)) = ((2nd ‘𝑝) · (2nd ‘𝑞)))
213	209, 212	opeq12d 4848	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) → ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩ = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
214	213, 22	ovmpoga 7546	. . . . . . . . . 10 ⊢ ((𝑝 ∈ (𝐵 × 𝑆) ∧ 𝑞 ∈ (𝐵 × 𝑆) ∧ ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
215	75, 79, 204, 214	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∼ 𝑝) ∧ 𝑣 ∼ 𝑞) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
216	202, 215	eqtrd 2765	. . . . . . . 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 5123	. . . . . . 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 257	. . . . . 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 466	. . . . 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 412	. . . 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 7407	. . . . . . 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 726	. . . . . 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 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑝 ∈ (𝐵 × 𝑆))
224		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑞 ∈ (𝐵 × 𝑆))
225	203	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ V)
226	223, 224, 225, 214	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) = ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩)
227	62	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑅 ∈ Ring)
228	223, 77	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (1st ‘𝑝) ∈ 𝐵)
229	224, 81	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (1st ‘𝑞) ∈ 𝐵)
230	8, 10, 227, 228, 229	ringcld 20176	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ((1st ‘𝑝) · (1st ‘𝑞)) ∈ 𝐵)
231	27	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
232	223, 92	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (2nd ‘𝑝) ∈ 𝑆)
233	224, 94	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (2nd ‘𝑞) ∈ 𝑆)
234	231, 232, 233, 96	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ((2nd ‘𝑝) · (2nd ‘𝑞)) ∈ 𝑆)
235	230, 234	opelxpd 5680	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ⟨((1st ‘𝑝) · (1st ‘𝑞)), ((2nd ‘𝑝) · (2nd ‘𝑞))⟩ ∈ (𝐵 × 𝑆))
236	226, 235	eqeltrd 2829	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)𝑞) ∈ (𝐵 × 𝑆))
237	222, 236	eqeltrd 2829	. . . . 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 466	. . . 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 17525	. . 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 1465	. 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 7407	. . . 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 770	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝑎 = ⟨𝐸, 𝐺⟩)
245	244	fveq2d 6865	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑎) = (1st ‘⟨𝐸, 𝐺⟩))
246	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐸 ∈ 𝐵)
247	2	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐺 ∈ 𝑆)
248		op1stg 7983	. . . . . . . . 9 ⊢ ((𝐸 ∈ 𝐵 ∧ 𝐺 ∈ 𝑆) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
249	246, 247, 248	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
250	245, 249	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑎) = 𝐸)
251		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝑏 = ⟨𝐹, 𝐻⟩)
252	251	fveq2d 6865	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑏) = (1st ‘⟨𝐹, 𝐻⟩))
253	4	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐹 ∈ 𝐵)
254	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐻 ∈ 𝑆)
255		op1stg 7983	. . . . . . . . 9 ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐻 ∈ 𝑆) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
256	253, 254, 255	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
257	252, 256	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘𝑏) = 𝐹)
258	250, 257	oveq12d 7408	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ((1st ‘𝑎) · (1st ‘𝑏)) = (𝐸 · 𝐹))
259	244	fveq2d 6865	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑎) = (2nd ‘⟨𝐸, 𝐺⟩))
260		op2ndg 7984	. . . . . . . . 9 ⊢ ((𝐸 ∈ 𝐵 ∧ 𝐺 ∈ 𝑆) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
261	246, 247, 260	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
262	259, 261	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑎) = 𝐺)
263	251	fveq2d 6865	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑏) = (2nd ‘⟨𝐹, 𝐻⟩))
264		op2ndg 7984	. . . . . . . . 9 ⊢ ((𝐹 ∈ 𝐵 ∧ 𝐻 ∈ 𝑆) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
265	253, 254, 264	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
266	263, 265	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘𝑏) = 𝐻)
267	262, 266	oveq12d 7408	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ((2nd ‘𝑎) · (2nd ‘𝑏)) = (𝐺 · 𝐻))
268	258, 267	opeq12d 4848	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩ = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
269		opex 5427	. . . . . 6 ⊢ ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩ ∈ V
270	269	a1i 11	. . . . 5 ⊢ (𝜑 → ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩ ∈ V)
271	243, 268, 3, 6, 270	ovmpod 7544	. . . 4 ⊢ (𝜑 → (⟨𝐸, 𝐺⟩(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st ‘𝑎) · (1st ‘𝑏)), ((2nd ‘𝑎) · (2nd ‘𝑏))⟩)⟨𝐹, 𝐻⟩) = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
272	242, 271	eqtrd 2765	. . 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 8714	. 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 2765	1 ⊢ (𝜑 → ([⟨𝐸, 𝐺⟩] ∼ ⊗ [⟨𝐹, 𝐻⟩] ∼ ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] ∼ )

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  ∅c0 4299  {csn 4592  {ctp 4596  ⟨cop 4598   class class class wbr 5110  {copab 5172   × cxp 5639  ‘cfv 6514  (class class class)co 7390   ∈ cmpo 7392  1^st c1st 7969  2^nd c2nd 7970  [cec 8672  1c1 11076  2c2 12248  ;cdc 12656  ndxcnx 17170  Basecbs 17186  +_gcplusg 17227  ._rcmulr 17228  Scalarcsca 17230   ·_𝑠 cvsca 17231  ·_𝑖cip 17232  TopSetcts 17233  lecple 17234  distcds 17236   ↾_t crest 17390  0_gc0g 17409   /_s cqus 17475  SubMndcsubmnd 18716  Grpcgrp 18872  -_gcsg 18874  CMndccmn 19717  mulGrpcmgp 20056  1_rcur 20097  Ringcrg 20149  CRingccrg 20150   ×_t ctx 23454   ~_RL cerl 33211   RLocal crloc 33212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-ec 8676  df-qs 8680  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9400  df-inf 9401  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-z 12537  df-dec 12657  df-uz 12801  df-fz 13476  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-0g 17411  df-imas 17478  df-qus 17479  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-submnd 18718  df-grp 18875  df-minusg 18876  df-sbg 18877  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-ring 20151  df-cring 20152  df-erl 33213  df-rloc 33214

This theorem is referenced by:  rloccring  33228  rloc1r  33230  rlocf1  33231  fracfld  33265  zringfrac  33532