Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rlocmulval Structured version   Visualization version   GIF version

Theorem rlocmulval 33255
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.
StepHypRef Expression
1 rlocaddval.6 . . . 4 (𝜑𝐸𝐵)
2 rlocaddval.8 . . . 4 (𝜑𝐺𝑆)
31, 2opelxpd 5727 . . 3 (𝜑 → ⟨𝐸, 𝐺⟩ ∈ (𝐵 × 𝑆))
4 rlocaddval.7 . . . 4 (𝜑𝐹𝐵)
5 rlocaddval.9 . . . 4 (𝜑𝐻𝑆)
64, 5opelxpd 5727 . . 3 (𝜑 → ⟨𝐹, 𝐻⟩ ∈ (𝐵 × 𝑆))
7 rlocaddval.4 . . . . 5 𝐿 = (𝑅 RLocal 𝑆)
8 rlocaddval.1 . . . . . 6 𝐵 = (Base‘𝑅)
9 eqid 2734 . . . . . 6 (0g𝑅) = (0g𝑅)
10 rlocaddval.2 . . . . . 6 · = (.r𝑅)
11 eqid 2734 . . . . . 6 (-g𝑅) = (-g𝑅)
12 rlocaddval.3 . . . . . 6 + = (+g𝑅)
13 eqid 2734 . . . . . 6 (le‘𝑅) = (le‘𝑅)
14 eqid 2734 . . . . . 6 (Scalar‘𝑅) = (Scalar‘𝑅)
15 eqid 2734 . . . . . 6 (Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅))
16 eqid 2734 . . . . . 6 ( ·𝑠𝑅) = ( ·𝑠𝑅)
17 eqid 2734 . . . . . 6 (𝐵 × 𝑆) = (𝐵 × 𝑆)
18 rlocaddval.5 . . . . . 6 = (𝑅 ~RL 𝑆)
19 eqid 2734 . . . . . 6 (TopSet‘𝑅) = (TopSet‘𝑅)
20 eqid 2734 . . . . . 6 (dist‘𝑅) = (dist‘𝑅)
21 eqid 2734 . . . . . 6 (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)
22 eqid 2734 . . . . . 6 (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)
23 eqid 2734 . . . . . 6 (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠𝑅)(1st𝑎)), (2nd𝑎)⟩) = (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠𝑅)(1st𝑎)), (2nd𝑎)⟩)
24 eqid 2734 . . . . . 6 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st𝑎) · (2nd𝑏))(le‘𝑅)((1st𝑏) · (2nd𝑎)))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st𝑎) · (2nd𝑏))(le‘𝑅)((1st𝑏) · (2nd𝑎)))}
25 eqid 2734 . . . . . 6 (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st𝑎) · (2nd𝑏))(dist‘𝑅)((1st𝑏) · (2nd𝑎)))) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st𝑎) · (2nd𝑏))(dist‘𝑅)((1st𝑏) · (2nd𝑎))))
26 rlocaddval.r . . . . . 6 (𝜑𝑅 ∈ CRing)
27 rlocaddval.s . . . . . . 7 (𝜑𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
28 eqid 2734 . . . . . . . . 9 (mulGrp‘𝑅) = (mulGrp‘𝑅)
2928, 8mgpbas 20157 . . . . . . . 8 𝐵 = (Base‘(mulGrp‘𝑅))
3029submss 18834 . . . . . . 7 (𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) → 𝑆𝐵)
3127, 30syl 17 . . . . . 6 (𝜑𝑆𝐵)
328, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 31rlocval 33245 . . . . 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 ))
337, 32eqtrid 2786 . . . 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 2735 . . . . . 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 2734 . . . . . . 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𝑎))))⟩})
3635imasvalstr 17497 . . . . . 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 17247 . . . . . 6 Base = Slot (Base‘ndx)
38 snsstp1 4820 . . . . . . 7 {⟨(Base‘ndx), (𝐵 × 𝑆)⟩} ⊆ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)⟩}
39 ssun1 4187 . . . . . . . 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 4187 . . . . . . . 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𝑎))))⟩})
4139, 40sstri 4004 . . . . . . 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𝑎))))⟩})
4238, 41sstri 4004 . . . . . 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𝑎))))⟩})
438fvexi 6920 . . . . . . . 8 𝐵 ∈ V
4443a1i 11 . . . . . . 7 (𝜑𝐵 ∈ V)
4544, 27xpexd 7769 . . . . . 6 (𝜑 → (𝐵 × 𝑆) ∈ V)
46 eqid 2734 . . . . . 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𝑎))))⟩}))
4734, 36, 37, 42, 45, 46strfv3 17238 . . . . 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𝑎))))⟩})) = (𝐵 × 𝑆))
4847eqcomd 2740 . . . 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 2734 . . . . 5 (1r𝑅) = (1r𝑅)
508, 9, 49, 10, 11, 17, 18, 26, 27erler 33251 . . . 4 (𝜑 Er (𝐵 × 𝑆))
51 tpex 7764 . . . . . . 7 {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)⟩} ∈ V
52 tpex 7764 . . . . . . 7 {⟨(Scalar‘ndx), (Scalar‘𝑅)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ (𝐵 × 𝑆) ↦ ⟨(𝑘( ·𝑠𝑅)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩} ∈ V
5351, 52unex 7762 . . . . . 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 7764 . . . . . 6 {⟨(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ((1st𝑎) · (2nd𝑏))(le‘𝑅)((1st𝑏) · (2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ (((1st𝑎) · (2nd𝑏))(dist‘𝑅)((1st𝑏) · (2nd𝑎))))⟩} ∈ V
5553, 54unex 7762 . . . . 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
5655a1i 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)
5731ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑆𝐵)
5857ad2antrr 726 . . . . . . . . . . 11 (((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) → 𝑆𝐵)
5958ad2antrr 726 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑆𝐵)
60 eqidd 2735 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ = ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩)
61 eqidd 2735 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩ = ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
6226crngringd 20263 . . . . . . . . . . . 12 (𝜑𝑅 ∈ Ring)
6362ad6antr 736 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑅 ∈ Ring)
64 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑢 𝑝)
658, 18, 57, 64erlcl1 33246 . . . . . . . . . . . . 13 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑢 ∈ (𝐵 × 𝑆))
6665ad4antr 732 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑢 ∈ (𝐵 × 𝑆))
67 xp1st 8044 . . . . . . . . . . . 12 (𝑢 ∈ (𝐵 × 𝑆) → (1st𝑢) ∈ 𝐵)
6866, 67syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (1st𝑢) ∈ 𝐵)
69 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑣 𝑞)
708, 18, 57, 69erlcl1 33246 . . . . . . . . . . . . 13 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑣 ∈ (𝐵 × 𝑆))
7170ad4antr 732 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑣 ∈ (𝐵 × 𝑆))
72 xp1st 8044 . . . . . . . . . . . 12 (𝑣 ∈ (𝐵 × 𝑆) → (1st𝑣) ∈ 𝐵)
7371, 72syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (1st𝑣) ∈ 𝐵)
748, 10, 63, 68, 73ringcld 20276 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑢) · (1st𝑣)) ∈ 𝐵)
758, 18, 57, 64erlcl2 33247 . . . . . . . . . . . . 13 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑝 ∈ (𝐵 × 𝑆))
7675ad4antr 732 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑝 ∈ (𝐵 × 𝑆))
77 xp1st 8044 . . . . . . . . . . . 12 (𝑝 ∈ (𝐵 × 𝑆) → (1st𝑝) ∈ 𝐵)
7876, 77syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (1st𝑝) ∈ 𝐵)
798, 18, 57, 69erlcl2 33247 . . . . . . . . . . . . 13 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑞 ∈ (𝐵 × 𝑆))
8079ad4antr 732 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑞 ∈ (𝐵 × 𝑆))
81 xp1st 8044 . . . . . . . . . . . 12 (𝑞 ∈ (𝐵 × 𝑆) → (1st𝑞) ∈ 𝐵)
8280, 81syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (1st𝑞) ∈ 𝐵)
838, 10, 63, 78, 82ringcld 20276 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑝) · (1st𝑞)) ∈ 𝐵)
8427ad6antr 736 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
85 xp2nd 8045 . . . . . . . . . . . 12 (𝑢 ∈ (𝐵 × 𝑆) → (2nd𝑢) ∈ 𝑆)
8666, 85syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑢) ∈ 𝑆)
87 xp2nd 8045 . . . . . . . . . . . 12 (𝑣 ∈ (𝐵 × 𝑆) → (2nd𝑣) ∈ 𝑆)
8871, 87syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑣) ∈ 𝑆)
8928, 10mgpplusg 20155 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘𝑅))
9089submcl 18837 . . . . . . . . . . 11 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (2nd𝑢) ∈ 𝑆 ∧ (2nd𝑣) ∈ 𝑆) → ((2nd𝑢) · (2nd𝑣)) ∈ 𝑆)
9184, 86, 88, 90syl3anc 1370 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((2nd𝑢) · (2nd𝑣)) ∈ 𝑆)
92 xp2nd 8045 . . . . . . . . . . . 12 (𝑝 ∈ (𝐵 × 𝑆) → (2nd𝑝) ∈ 𝑆)
9376, 92syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑝) ∈ 𝑆)
94 xp2nd 8045 . . . . . . . . . . . 12 (𝑞 ∈ (𝐵 × 𝑆) → (2nd𝑞) ∈ 𝑆)
9580, 94syl 17 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑞) ∈ 𝑆)
9689submcl 18837 . . . . . . . . . . 11 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ (2nd𝑝) ∈ 𝑆 ∧ (2nd𝑞) ∈ 𝑆) → ((2nd𝑝) · (2nd𝑞)) ∈ 𝑆)
9784, 93, 95, 96syl3anc 1370 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((2nd𝑝) · (2nd𝑞)) ∈ 𝑆)
98 simp-4r 784 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑓𝑆)
99 simplr 769 . . . . . . . . . . 11 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑔𝑆)
10089submcl 18837 . . . . . . . . . . 11 ((𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑓𝑆𝑔𝑆) → (𝑓 · 𝑔) ∈ 𝑆)
10184, 98, 99, 100syl3anc 1370 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑓 · 𝑔) ∈ 𝑆)
10259, 101sseldd 3995 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑓 · 𝑔) ∈ 𝐵)
10359, 97sseldd 3995 . . . . . . . . . . . . 13 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((2nd𝑝) · (2nd𝑞)) ∈ 𝐵)
1048, 10, 63, 74, 103ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((1st𝑢) · (1st𝑣)) · ((2nd𝑝) · (2nd𝑞))) ∈ 𝐵)
10559, 91sseldd 3995 . . . . . . . . . . . . 13 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((2nd𝑢) · (2nd𝑣)) ∈ 𝐵)
1068, 10, 63, 83, 105ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣))) ∈ 𝐵)
1078, 10, 11, 63, 102, 104, 106ringsubdi 20320 . . . . . . . . . . 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𝑣))))))
10863ringgrpd 20259 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑅 ∈ Grp)
1098, 10, 63, 102, 104ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑢) · (1st𝑣)) · ((2nd𝑝) · (2nd𝑞)))) ∈ 𝐵)
1108, 10, 63, 78, 73ringcld 20276 . . . . . . . . . . . . . 14 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑝) · (1st𝑣)) ∈ 𝐵)
11159, 86sseldd 3995 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑢) ∈ 𝐵)
11259, 95sseldd 3995 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑞) ∈ 𝐵)
1138, 10, 63, 111, 112ringcld 20276 . . . . . . . . . . . . . 14 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((2nd𝑢) · (2nd𝑞)) ∈ 𝐵)
1148, 10, 63, 110, 113ringcld 20276 . . . . . . . . . . . . 13 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞))) ∈ 𝐵)
1158, 10, 63, 102, 114ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞)))) ∈ 𝐵)
1168, 10, 63, 102, 106ringcld 20276 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣)))) ∈ 𝐵)
1178, 12, 11grpnpncan 19065 . . . . . . . . . . . 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𝑣))))))
118108, 109, 115, 116, 117syl13anc 1371 . . . . . . . . . . 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𝑣))))))
11926ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → 𝑅 ∈ CRing)
120119ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) → 𝑅 ∈ CRing)
121120ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑅 ∈ CRing)
12228crngmgp 20258 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
123121, 122syl 17 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (mulGrp‘𝑅) ∈ CMnd)
12459, 98sseldd 3995 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑓𝐵)
12559, 99sseldd 3995 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → 𝑔𝐵)
12659, 93sseldd 3995 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑝) ∈ 𝐵)
12729, 89, 123, 124, 125, 68, 73, 126, 112cmn246135 33020 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑢) · (1st𝑣)) · ((2nd𝑝) · (2nd𝑞)))) = ((𝑔 · ((1st𝑣) · (2nd𝑞))) · (𝑓 · ((1st𝑢) · (2nd𝑝)))))
12829, 89, 123, 124, 125, 78, 73, 111, 112cmn246135 33020 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞)))) = ((𝑔 · ((1st𝑣) · (2nd𝑞))) · (𝑓 · ((1st𝑝) · (2nd𝑢)))))
129127, 128oveq12d 7448 . . . . . . . . . . . . . 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𝑢))))))
1308, 10, 63, 73, 112ringcld 20276 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑣) · (2nd𝑞)) ∈ 𝐵)
1318, 10, 63, 125, 130ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑔 · ((1st𝑣) · (2nd𝑞))) ∈ 𝐵)
1328, 10, 63, 68, 126ringcld 20276 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑢) · (2nd𝑝)) ∈ 𝐵)
1338, 10, 63, 124, 132ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑓 · ((1st𝑢) · (2nd𝑝))) ∈ 𝐵)
1348, 10, 63, 78, 111ringcld 20276 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑝) · (2nd𝑢)) ∈ 𝐵)
1358, 10, 63, 124, 134ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑓 · ((1st𝑝) · (2nd𝑢))) ∈ 𝐵)
1368, 10, 11, 63, 131, 133, 135ringsubdi 20320 . . . . . . . . . . . . . . 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𝑢))))))
1378, 10, 11, 63, 124, 132, 134ringsubdi 20320 . . . . . . . . . . . . . . . . . 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 776 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅))
139137, 138eqtr3d 2776 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · ((1st𝑢) · (2nd𝑝)))(-g𝑅)(𝑓 · ((1st𝑝) · (2nd𝑢)))) = (0g𝑅))
140139oveq2d 7446 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑔 · ((1st𝑣) · (2nd𝑞))) · ((𝑓 · ((1st𝑢) · (2nd𝑝)))(-g𝑅)(𝑓 · ((1st𝑝) · (2nd𝑢))))) = ((𝑔 · ((1st𝑣) · (2nd𝑞))) · (0g𝑅)))
1418, 10, 9, 63, 131ringrzd 20309 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑔 · ((1st𝑣) · (2nd𝑞))) · (0g𝑅)) = (0g𝑅))
142140, 141eqtrd 2774 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑔 · ((1st𝑣) · (2nd𝑞))) · ((𝑓 · ((1st𝑢) · (2nd𝑝)))(-g𝑅)(𝑓 · ((1st𝑝) · (2nd𝑢))))) = (0g𝑅))
143136, 142eqtr3d 2776 . . . . . . . . . . . . . 14 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((𝑔 · ((1st𝑣) · (2nd𝑞))) · (𝑓 · ((1st𝑢) · (2nd𝑝))))(-g𝑅)((𝑔 · ((1st𝑣) · (2nd𝑞))) · (𝑓 · ((1st𝑝) · (2nd𝑢))))) = (0g𝑅))
144129, 143eqtrd 2774 . . . . . . . . . . . . 13 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((𝑓 · 𝑔) · (((1st𝑢) · (1st𝑣)) · ((2nd𝑝) · (2nd𝑞))))(-g𝑅)((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞))))) = (0g𝑅))
1458, 10, 121, 78, 73crngcomd 20272 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑝) · (1st𝑣)) = ((1st𝑣) · (1st𝑝)))
146145oveq1d 7445 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞))) = (((1st𝑣) · (1st𝑝)) · ((2nd𝑢) · (2nd𝑞))))
147146oveq2d 7446 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞)))) = ((𝑓 · 𝑔) · (((1st𝑣) · (1st𝑝)) · ((2nd𝑢) · (2nd𝑞)))))
14829, 89, 123, 124, 125, 73, 78, 111, 112cmn145236 33021 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑣) · (1st𝑝)) · ((2nd𝑢) · (2nd𝑞)))) = ((𝑓 · ((1st𝑝) · (2nd𝑢))) · (𝑔 · ((1st𝑣) · (2nd𝑞)))))
149147, 148eqtrd 2774 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞)))) = ((𝑓 · ((1st𝑝) · (2nd𝑢))) · (𝑔 · ((1st𝑣) · (2nd𝑞)))))
1508, 10, 121, 82, 78crngcomd 20272 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑞) · (1st𝑝)) = ((1st𝑝) · (1st𝑞)))
151150oveq1d 7445 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((1st𝑞) · (1st𝑝)) · ((2nd𝑢) · (2nd𝑣))) = (((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣))))
152151oveq2d 7446 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑞) · (1st𝑝)) · ((2nd𝑢) · (2nd𝑣)))) = ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣)))))
15359, 88sseldd 3995 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (2nd𝑣) ∈ 𝐵)
15429, 89, 123, 124, 125, 82, 78, 111, 153cmn145236 33021 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑞) · (1st𝑝)) · ((2nd𝑢) · (2nd𝑣)))) = ((𝑓 · ((1st𝑝) · (2nd𝑢))) · (𝑔 · ((1st𝑞) · (2nd𝑣)))))
155152, 154eqtr3d 2776 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣)))) = ((𝑓 · ((1st𝑝) · (2nd𝑢))) · (𝑔 · ((1st𝑞) · (2nd𝑣)))))
156149, 155oveq12d 7448 . . . . . . . . . . . . . 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𝑣))))))
1578, 10, 63, 82, 153ringcld 20276 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((1st𝑞) · (2nd𝑣)) ∈ 𝐵)
1588, 10, 11, 63, 125, 130, 157ringsubdi 20320 . . . . . . . . . . . . . . . . 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𝑅))
160158, 159eqtr3d 2776 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑔 · ((1st𝑣) · (2nd𝑞)))(-g𝑅)(𝑔 · ((1st𝑞) · (2nd𝑣)))) = (0g𝑅))
161160oveq2d 7446 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · ((1st𝑝) · (2nd𝑢))) · ((𝑔 · ((1st𝑣) · (2nd𝑞)))(-g𝑅)(𝑔 · ((1st𝑞) · (2nd𝑣))))) = ((𝑓 · ((1st𝑝) · (2nd𝑢))) · (0g𝑅)))
1628, 10, 63, 125, 157ringcld 20276 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (𝑔 · ((1st𝑞) · (2nd𝑣))) ∈ 𝐵)
1638, 10, 11, 63, 135, 131, 162ringsubdi 20320 . . . . . . . . . . . . . . 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𝑣))))))
1648, 10, 9, 63, 135ringrzd 20309 . . . . . . . . . . . . . . 15 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · ((1st𝑝) · (2nd𝑢))) · (0g𝑅)) = (0g𝑅))
165161, 163, 1643eqtr3d 2782 . . . . . . . . . . . . . 14 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((𝑓 · ((1st𝑝) · (2nd𝑢))) · (𝑔 · ((1st𝑣) · (2nd𝑞))))(-g𝑅)((𝑓 · ((1st𝑝) · (2nd𝑢))) · (𝑔 · ((1st𝑞) · (2nd𝑣))))) = (0g𝑅))
166156, 165eqtrd 2774 . . . . . . . . . . . . 13 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑣)) · ((2nd𝑢) · (2nd𝑞))))(-g𝑅)((𝑓 · 𝑔) · (((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣))))) = (0g𝑅))
167144, 166oveq12d 7448 . . . . . . . . . . . 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𝑅)))
1688, 9grpidcl 18995 . . . . . . . . . . . . . 14 (𝑅 ∈ Grp → (0g𝑅) ∈ 𝐵)
169108, 168syl 17 . . . . . . . . . . . . 13 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → (0g𝑅) ∈ 𝐵)
1708, 12, 9, 108, 169grplidd 18999 . . . . . . . . . . . 12 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((0g𝑅) + (0g𝑅)) = (0g𝑅))
171167, 170eqtrd 2774 . . . . . . . . . . 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𝑅))
172107, 118, 1713eqtr2d 2780 . . . . . . . . . 10 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ((𝑓 · 𝑔) · ((((1st𝑢) · (1st𝑣)) · ((2nd𝑝) · (2nd𝑞)))(-g𝑅)(((1st𝑝) · (1st𝑞)) · ((2nd𝑢) · (2nd𝑣))))) = (0g𝑅))
1738, 18, 59, 9, 10, 11, 60, 61, 74, 83, 91, 97, 101, 172erlbrd 33249 . . . . . . . . 9 (((((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) ∧ 𝑔𝑆) ∧ (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅)) → ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
17469ad2antrr 726 . . . . . . . . . 10 (((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) → 𝑣 𝑞)
1758, 18, 58, 9, 10, 11, 174erldi 33248 . . . . . . . . 9 (((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) → ∃𝑔𝑆 (𝑔 · (((1st𝑣) · (2nd𝑞))(-g𝑅)((1st𝑞) · (2nd𝑣)))) = (0g𝑅))
176173, 175r19.29a 3159 . . . . . . . 8 (((((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) ∧ 𝑓𝑆) ∧ (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅)) → ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
1778, 18, 57, 9, 10, 11, 64erldi 33248 . . . . . . . 8 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → ∃𝑓𝑆 (𝑓 · (((1st𝑢) · (2nd𝑝))(-g𝑅)((1st𝑝) · (2nd𝑢)))) = (0g𝑅))
178176, 177r19.29a 3159 . . . . . . 7 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
179 mulridx 17339 . . . . . . . . . . . 12 .r = Slot (.r‘ndx)
180 snsstp3 4822 . . . . . . . . . . . . 13 {⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)⟩} ⊆ {⟨(Base‘ndx), (𝐵 × 𝑆)⟩, ⟨(+g‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)⟩}
181180, 41sstri 4004 . . . . . . . . . . . 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𝑎))))⟩})
18222mpoexg 8099 . . . . . . . . . . . . 13 (((𝐵 × 𝑆) ∈ V ∧ (𝐵 × 𝑆) ∈ V) → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩) ∈ V)
18345, 45, 182syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩) ∈ V)
184 eqid 2734 . . . . . . . . . . . 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𝑎))))⟩}))
18534, 36, 179, 181, 183, 184strfv3 17238 . . . . . . . . . . 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𝑏))⟩))
186185ad2antrr 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𝑏))⟩))
187186oveqd 7447 . . . . . . . . 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 5474 . . . . . . . . . . 11 ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ ∈ V
189188a1i 11 . . . . . . . . . 10 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ ∈ V)
190 simpl 482 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑎 = 𝑢)
191190fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑣) → (1st𝑎) = (1st𝑢))
192 simpr 484 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑏 = 𝑣)
193192fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑣) → (1st𝑏) = (1st𝑣))
194191, 193oveq12d 7448 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑣) → ((1st𝑎) · (1st𝑏)) = ((1st𝑢) · (1st𝑣)))
195190fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑣) → (2nd𝑎) = (2nd𝑢))
196192fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑣) → (2nd𝑏) = (2nd𝑣))
197195, 196oveq12d 7448 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑣) → ((2nd𝑎) · (2nd𝑏)) = ((2nd𝑢) · (2nd𝑣)))
198194, 197opeq12d 4885 . . . . . . . . . . 11 ((𝑎 = 𝑢𝑏 = 𝑣) → ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩ = ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩)
199198, 22ovmpoga 7586 . . . . . . . . . 10 ((𝑢 ∈ (𝐵 × 𝑆) ∧ 𝑣 ∈ (𝐵 × 𝑆) ∧ ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩ ∈ V) → (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)𝑣) = ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩)
20065, 70, 189, 199syl3anc 1370 . . . . . . . . 9 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → (𝑢(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)𝑣) = ⟨((1st𝑢) · (1st𝑣)), ((2nd𝑢) · (2nd𝑣))⟩)
201187, 200eqtrd 2774 . . . . . . . 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𝑣))⟩)
202186oveqd 7447 . . . . . . . . 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 5474 . . . . . . . . . . 11 ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩ ∈ V
204203a1i 11 . . . . . . . . . 10 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩ ∈ V)
205 simpl 482 . . . . . . . . . . . . . 14 ((𝑎 = 𝑝𝑏 = 𝑞) → 𝑎 = 𝑝)
206205fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑝𝑏 = 𝑞) → (1st𝑎) = (1st𝑝))
207 simpr 484 . . . . . . . . . . . . . 14 ((𝑎 = 𝑝𝑏 = 𝑞) → 𝑏 = 𝑞)
208207fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑝𝑏 = 𝑞) → (1st𝑏) = (1st𝑞))
209206, 208oveq12d 7448 . . . . . . . . . . . 12 ((𝑎 = 𝑝𝑏 = 𝑞) → ((1st𝑎) · (1st𝑏)) = ((1st𝑝) · (1st𝑞)))
210205fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑝𝑏 = 𝑞) → (2nd𝑎) = (2nd𝑝))
211207fveq2d 6910 . . . . . . . . . . . . 13 ((𝑎 = 𝑝𝑏 = 𝑞) → (2nd𝑏) = (2nd𝑞))
212210, 211oveq12d 7448 . . . . . . . . . . . 12 ((𝑎 = 𝑝𝑏 = 𝑞) → ((2nd𝑎) · (2nd𝑏)) = ((2nd𝑝) · (2nd𝑞)))
213209, 212opeq12d 4885 . . . . . . . . . . 11 ((𝑎 = 𝑝𝑏 = 𝑞) → ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩ = ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
214213, 22ovmpoga 7586 . . . . . . . . . 10 ((𝑝 ∈ (𝐵 × 𝑆) ∧ 𝑞 ∈ (𝐵 × 𝑆) ∧ ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩ ∈ V) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)𝑞) = ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
21575, 79, 204, 214syl3anc 1370 . . . . . . . . 9 (((𝜑𝑢 𝑝) ∧ 𝑣 𝑞) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)𝑞) = ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
216202, 215eqtrd 2774 . . . . . . . 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𝑞))⟩)
217201, 216breq12d 5160 . . . . . . 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𝑞))⟩))
218178, 217mpbird 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𝑎))))⟩}))𝑞))
219218anasss 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𝑎))))⟩}))𝑞))
220219ex 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𝑎))))⟩}))𝑞)))
221185oveqd 7447 . . . . . . 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𝑏))⟩)𝑞))
222221ad2antrr 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 769 . . . . . . . 8 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑝 ∈ (𝐵 × 𝑆))
224 simpr 484 . . . . . . . 8 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑞 ∈ (𝐵 × 𝑆))
225203a1i 11 . . . . . . . 8 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩ ∈ V)
226223, 224, 225, 214syl3anc 1370 . . . . . . 7 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)𝑞) = ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩)
22762ad2antrr 726 . . . . . . . . 9 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑅 ∈ Ring)
228223, 77syl 17 . . . . . . . . 9 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (1st𝑝) ∈ 𝐵)
229224, 81syl 17 . . . . . . . . 9 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (1st𝑞) ∈ 𝐵)
2308, 10, 227, 228, 229ringcld 20276 . . . . . . . 8 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ((1st𝑝) · (1st𝑞)) ∈ 𝐵)
23127ad2antrr 726 . . . . . . . . 9 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → 𝑆 ∈ (SubMnd‘(mulGrp‘𝑅)))
232223, 92syl 17 . . . . . . . . 9 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (2nd𝑝) ∈ 𝑆)
233224, 94syl 17 . . . . . . . . 9 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (2nd𝑞) ∈ 𝑆)
234231, 232, 233, 96syl3anc 1370 . . . . . . . 8 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ((2nd𝑝) · (2nd𝑞)) ∈ 𝑆)
235230, 234opelxpd 5727 . . . . . . 7 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → ⟨((1st𝑝) · (1st𝑞)), ((2nd𝑝) · (2nd𝑞))⟩ ∈ (𝐵 × 𝑆))
236226, 235eqeltrd 2838 . . . . . 6 (((𝜑𝑝 ∈ (𝐵 × 𝑆)) ∧ 𝑞 ∈ (𝐵 × 𝑆)) → (𝑝(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)𝑞) ∈ (𝐵 × 𝑆))
237222, 236eqeltrd 2838 . . . . 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𝑎))))⟩}))𝑞) ∈ (𝐵 × 𝑆))
238237anasss 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𝐿)
24033, 48, 50, 56, 220, 238, 184, 239qusmulval 17601 . . 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𝑎))))⟩}))⟨𝐹, 𝐻⟩)] )
2413, 6, 240mpd3an23 1462 . 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𝑎))))⟩}))⟨𝐹, 𝐻⟩)] )
242185oveqd 7447 . . . 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𝑏))⟩)⟨𝐹, 𝐻⟩))
24322a1i 11 . . . . 5 (𝜑 → (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩) = (𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩))
244 simprl 771 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝑎 = ⟨𝐸, 𝐺⟩)
245244fveq2d 6910 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st𝑎) = (1st ‘⟨𝐸, 𝐺⟩))
2461adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐸𝐵)
2472adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐺𝑆)
248 op1stg 8024 . . . . . . . . 9 ((𝐸𝐵𝐺𝑆) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
249246, 247, 248syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘⟨𝐸, 𝐺⟩) = 𝐸)
250245, 249eqtrd 2774 . . . . . . 7 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st𝑎) = 𝐸)
251 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝑏 = ⟨𝐹, 𝐻⟩)
252251fveq2d 6910 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st𝑏) = (1st ‘⟨𝐹, 𝐻⟩))
2534adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐹𝐵)
2545adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → 𝐻𝑆)
255 op1stg 8024 . . . . . . . . 9 ((𝐹𝐵𝐻𝑆) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
256253, 254, 255syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st ‘⟨𝐹, 𝐻⟩) = 𝐹)
257252, 256eqtrd 2774 . . . . . . 7 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (1st𝑏) = 𝐹)
258250, 257oveq12d 7448 . . . . . 6 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ((1st𝑎) · (1st𝑏)) = (𝐸 · 𝐹))
259244fveq2d 6910 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd𝑎) = (2nd ‘⟨𝐸, 𝐺⟩))
260 op2ndg 8025 . . . . . . . . 9 ((𝐸𝐵𝐺𝑆) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
261246, 247, 260syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘⟨𝐸, 𝐺⟩) = 𝐺)
262259, 261eqtrd 2774 . . . . . . 7 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd𝑎) = 𝐺)
263251fveq2d 6910 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd𝑏) = (2nd ‘⟨𝐹, 𝐻⟩))
264 op2ndg 8025 . . . . . . . . 9 ((𝐹𝐵𝐻𝑆) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
265253, 254, 264syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd ‘⟨𝐹, 𝐻⟩) = 𝐻)
266263, 265eqtrd 2774 . . . . . . 7 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → (2nd𝑏) = 𝐻)
267262, 266oveq12d 7448 . . . . . 6 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ((2nd𝑎) · (2nd𝑏)) = (𝐺 · 𝐻))
268258, 267opeq12d 4885 . . . . 5 ((𝜑 ∧ (𝑎 = ⟨𝐸, 𝐺⟩ ∧ 𝑏 = ⟨𝐹, 𝐻⟩)) → ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩ = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
269 opex 5474 . . . . . 6 ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩ ∈ V
270269a1i 11 . . . . 5 (𝜑 → ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩ ∈ V)
271243, 268, 3, 6, 270ovmpod 7584 . . . 4 (𝜑 → (⟨𝐸, 𝐺⟩(𝑎 ∈ (𝐵 × 𝑆), 𝑏 ∈ (𝐵 × 𝑆) ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)⟨𝐹, 𝐻⟩) = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
272242, 271eqtrd 2774 . . 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𝑎))))⟩}))⟨𝐹, 𝐻⟩) = ⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩)
273272eceq1d 8783 . 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𝑎))))⟩}))⟨𝐹, 𝐻⟩)] = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] )
274241, 273eqtrd 2774 1 (𝜑 → ([⟨𝐸, 𝐺⟩] [⟨𝐹, 𝐻⟩] ) = [⟨(𝐸 · 𝐹), (𝐺 · 𝐻)⟩] )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  Vcvv 3477  cun 3960  wss 3962  c0 4338  {csn 4630  {ctp 4634  cop 4636   class class class wbr 5147  {copab 5209   × cxp 5686  cfv 6562  (class class class)co 7430  cmpo 7432  1st c1st 8010  2nd c2nd 8011  [cec 8741  1c1 11153  2c2 12318  cdc 12730  ndxcnx 17226  Basecbs 17244  +gcplusg 17297  .rcmulr 17298  Scalarcsca 17300   ·𝑠 cvsca 17301  ·𝑖cip 17302  TopSetcts 17303  lecple 17304  distcds 17306  t crest 17466  0gc0g 17485   /s cqus 17551  SubMndcsubmnd 18807  Grpcgrp 18963  -gcsg 18965  CMndccmn 19812  mulGrpcmgp 20151  1rcur 20198  Ringcrg 20250  CRingccrg 20251   ×t ctx 23583   ~RL cerl 33239   RLocal crloc 33240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-ec 8745  df-qs 8749  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-fz 13544  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-0g 17487  df-imas 17554  df-qus 17555  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-cring 20253  df-erl 33241  df-rloc 33242
This theorem is referenced by:  rloccring  33256  rloc1r  33258  rlocf1  33259  fracfld  33289  zringfrac  33561
  Copyright terms: Public domain W3C validator