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 |
⊢ ( 𝜑 → ( [ 〈 𝐸 , 𝐺 〉 ] ∼ ⊗ [ 〈 𝐹 , 𝐻 〉 ] ∼ ) = [ 〈 ( 𝐸 · 𝐹 ) , ( 𝐺 · 𝐻 ) 〉 ] ∼ ) |