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