Step | Hyp | Ref
| Expression |
1 | | 0sno 27565 |
. . 3
⊢
0s ∈ No |
2 | | mulsval 27805 |
. . 3
⊢ ((𝐴 ∈
No ∧ 0s ∈ No ) →
(𝐴 ·s
0s ) = (({𝑎
∣ ∃𝑝 ∈ ( L
‘𝐴)∃𝑞 ∈ ( L ‘
0s )𝑎 = (((𝑝 ·s
0s ) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘ 0s )𝑏 = (((𝑟 ·s 0s )
+s (𝐴
·s 𝑠))
-s (𝑟
·s 𝑠))})
|s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
3 | 1, 2 | mpan2 688 |
. 2
⊢ (𝐴 ∈
No → (𝐴
·s 0s ) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘ 0s )𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝐴)∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
4 | | rex0 4357 |
. . . . . . . . . 10
⊢ ¬
∃𝑞 ∈ ∅
𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞)) |
5 | | left0s 27625 |
. . . . . . . . . . 11
⊢ ( L
‘ 0s ) = ∅ |
6 | 5 | rexeqi 3323 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈ ( L
‘ 0s )𝑎 =
(((𝑝 ·s
0s ) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑞 ∈ ∅ 𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))) |
7 | 4, 6 | mtbir 323 |
. . . . . . . . 9
⊢ ¬
∃𝑞 ∈ ( L ‘
0s )𝑎 = (((𝑝 ·s
0s ) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑝 ∈ ( L ‘𝐴) → ¬ ∃𝑞 ∈ ( L ‘
0s )𝑎 = (((𝑝 ·s
0s ) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))) |
9 | 8 | nrex 3073 |
. . . . . . 7
⊢ ¬
∃𝑝 ∈ ( L
‘𝐴)∃𝑞 ∈ ( L ‘
0s )𝑎 = (((𝑝 ·s
0s ) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞)) |
10 | 9 | abf 4402 |
. . . . . 6
⊢ {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘ 0s )𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))} =
∅ |
11 | | rex0 4357 |
. . . . . . . . . 10
⊢ ¬
∃𝑠 ∈ ∅
𝑏 = (((𝑟 ·s 0s )
+s (𝐴
·s 𝑠))
-s (𝑟
·s 𝑠)) |
12 | | right0s 27626 |
. . . . . . . . . . 11
⊢ ( R
‘ 0s ) = ∅ |
13 | 12 | rexeqi 3323 |
. . . . . . . . . 10
⊢
(∃𝑠 ∈ ( R
‘ 0s )𝑏 =
(((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑠 ∈ ∅ 𝑏 = (((𝑟 ·s 0s )
+s (𝐴
·s 𝑠))
-s (𝑟
·s 𝑠))) |
14 | 11, 13 | mtbir 323 |
. . . . . . . . 9
⊢ ¬
∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝑟 ∈ ( R ‘𝐴) → ¬ ∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
16 | 15 | nrex 3073 |
. . . . . . 7
⊢ ¬
∃𝑟 ∈ ( R
‘𝐴)∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠)) |
17 | 16 | abf 4402 |
. . . . . 6
⊢ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘ 0s )𝑏 = (((𝑟 ·s 0s )
+s (𝐴
·s 𝑠))
-s (𝑟
·s 𝑠))} =
∅ |
18 | 10, 17 | uneq12i 4161 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘ 0s )𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝐴)∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = (∅ ∪
∅) |
19 | | un0 4390 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
20 | 18, 19 | eqtri 2759 |
. . . 4
⊢ ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘ 0s )𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝐴)∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = ∅ |
21 | | rex0 4357 |
. . . . . . . . . 10
⊢ ¬
∃𝑢 ∈ ∅
𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢)) |
22 | 12 | rexeqi 3323 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈ ( R
‘ 0s )𝑐 =
(((𝑡 ·s
0s ) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑢 ∈ ∅ 𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))) |
23 | 21, 22 | mtbir 323 |
. . . . . . . . 9
⊢ ¬
∃𝑢 ∈ ( R ‘
0s )𝑐 = (((𝑡 ·s
0s ) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (𝑡 ∈ ( L ‘𝐴) → ¬ ∃𝑢 ∈ ( R ‘
0s )𝑐 = (((𝑡 ·s
0s ) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))) |
25 | 24 | nrex 3073 |
. . . . . . 7
⊢ ¬
∃𝑡 ∈ ( L
‘𝐴)∃𝑢 ∈ ( R ‘
0s )𝑐 = (((𝑡 ·s
0s ) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢)) |
26 | 25 | abf 4402 |
. . . . . 6
⊢ {𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))} =
∅ |
27 | | rex0 4357 |
. . . . . . . . . 10
⊢ ¬
∃𝑤 ∈ ∅
𝑑 = (((𝑣 ·s 0s )
+s (𝐴
·s 𝑤))
-s (𝑣
·s 𝑤)) |
28 | 5 | rexeqi 3323 |
. . . . . . . . . 10
⊢
(∃𝑤 ∈ ( L
‘ 0s )𝑑 =
(((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑤 ∈ ∅ 𝑑 = (((𝑣 ·s 0s )
+s (𝐴
·s 𝑤))
-s (𝑣
·s 𝑤))) |
29 | 27, 28 | mtbir 323 |
. . . . . . . . 9
⊢ ¬
∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (𝑣 ∈ ( R ‘𝐴) → ¬ ∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))) |
31 | 30 | nrex 3073 |
. . . . . . 7
⊢ ¬
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤)) |
32 | 31 | abf 4402 |
. . . . . 6
⊢ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘ 0s )𝑑 = (((𝑣 ·s 0s )
+s (𝐴
·s 𝑤))
-s (𝑣
·s 𝑤))} =
∅ |
33 | 26, 32 | uneq12i 4161 |
. . . . 5
⊢ ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = (∅ ∪
∅) |
34 | 33, 19 | eqtri 2759 |
. . . 4
⊢ ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ∅ |
35 | 20, 34 | oveq12i 7424 |
. . 3
⊢ (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘ 0s )𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝐴)∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) = (∅ |s ∅) |
36 | | df-0s 27563 |
. . 3
⊢
0s = (∅ |s ∅) |
37 | 35, 36 | eqtr4i 2762 |
. 2
⊢ (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝐴)∃𝑞 ∈ ( L ‘ 0s )𝑎 = (((𝑝 ·s 0s )
+s (𝐴
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝐴)∃𝑠 ∈ ( R ‘
0s )𝑏 = (((𝑟 ·s
0s ) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘ 0s )𝑐 = (((𝑡 ·s 0s )
+s (𝐴
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝐴)∃𝑤 ∈ ( L ‘
0s )𝑑 = (((𝑣 ·s
0s ) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) = 0s |
38 | 3, 37 | eqtrdi 2787 |
1
⊢ (𝐴 ∈
No → (𝐴
·s 0s ) = 0s ) |