Metamath Proof Explorer


Theorem rlocmulval

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

Ref Expression
Hypotheses 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 rlocmulval ( 𝜑 → ( [ ⟨ 𝐸 , 𝐺 ⟩ ] [ ⟨ 𝐹 , 𝐻 ⟩ ] ) = [ ⟨ ( 𝐸 · 𝐹 ) , ( 𝐺 · 𝐻 ) ⟩ ] )

Proof

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