Step | Hyp | Ref
| Expression |
1 | | oveq1 7408 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s
1s ) = (𝑥𝑂 ·s
1s )) |
2 | | id 22 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → 𝑥 = 𝑥𝑂) |
3 | 1, 2 | eqeq12d 2740 |
. 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s
1s ) = 𝑥 ↔
(𝑥𝑂
·s 1s ) = 𝑥𝑂)) |
4 | | oveq1 7408 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ·s 1s ) =
(𝐴 ·s
1s )) |
5 | | id 22 |
. . 3
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
6 | 4, 5 | eqeq12d 2740 |
. 2
⊢ (𝑥 = 𝐴 → ((𝑥 ·s 1s ) = 𝑥 ↔ (𝐴 ·s 1s ) =
𝐴)) |
7 | | 1sno 27675 |
. . . . . 6
⊢
1s ∈ No |
8 | | mulsval 27924 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ 1s ∈ No ) →
(𝑥 ·s
1s ) = (({𝑎
∣ ∃𝑝 ∈ ( L
‘𝑥)∃𝑞 ∈ ( L ‘
1s )𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘ 1s )𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠))})
|s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
9 | 7, 8 | mpan2 688 |
. . . . 5
⊢ (𝑥 ∈
No → (𝑥
·s 1s ) = (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (𝑥 ·s
1s ) = (({𝑎
∣ ∃𝑝 ∈ ( L
‘𝑥)∃𝑞 ∈ ( L ‘
1s )𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘ 1s )𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠))})
|s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
11 | | elun1 4168 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ ( L ‘𝑥) → 𝑝 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
12 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s
1s ) = (𝑝
·s 1s )) |
13 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑝 → 𝑥𝑂 = 𝑝) |
14 | 12, 13 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s
1s ) = 𝑥𝑂 ↔ (𝑝 ·s
1s ) = 𝑝)) |
15 | 14 | rspcva 3602 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑝 ·s
1s ) = 𝑝) |
16 | 11, 15 | sylan 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ( L ‘𝑥) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑝 ·s
1s ) = 𝑝) |
17 | 16 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂 ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 ·s 1s ) = 𝑝) |
18 | 17 | adantll 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 ·s 1s ) = 𝑝) |
19 | | muls01 27927 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
No → (𝑥
·s 0s ) = 0s ) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (𝑥 ·s
0s ) = 0s ) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑥 ·s 0s ) =
0s ) |
22 | 18, 21 | oveq12d 7419 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → ((𝑝 ·s 1s )
+s (𝑥
·s 0s )) = (𝑝 +s 0s
)) |
23 | | leftssno 27722 |
. . . . . . . . . . . . . . . . . 18
⊢ ( L
‘𝑥) ⊆ No |
24 | 23 | sseli 3970 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ( L ‘𝑥) → 𝑝 ∈ No
) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → 𝑝 ∈ No
) |
26 | 25 | addsridd 27797 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 +s 0s ) = 𝑝) |
27 | 22, 26 | eqtrd 2764 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → ((𝑝 ·s 1s )
+s (𝑥
·s 0s )) = 𝑝) |
28 | | muls01 27927 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈
No → (𝑝
·s 0s ) = 0s ) |
29 | 25, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 ·s 0s ) =
0s ) |
30 | 27, 29 | oveq12d 7419 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) =
(𝑝 -s
0s )) |
31 | | subsid1 27891 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈
No → (𝑝
-s 0s ) = 𝑝) |
32 | 25, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 -s 0s ) = 𝑝) |
33 | 30, 32 | eqtrd 2764 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) =
𝑝) |
34 | 33 | eqeq2d 2735 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) ↔
𝑎 = 𝑝)) |
35 | | equcom 2013 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑝 ↔ 𝑝 = 𝑎) |
36 | 34, 35 | bitrdi 287 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) ↔
𝑝 = 𝑎)) |
37 | 36 | rexbidva 3168 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) ↔
∃𝑝 ∈ ( L
‘𝑥)𝑝 = 𝑎)) |
38 | | left1s 27736 |
. . . . . . . . . . . 12
⊢ ( L
‘ 1s ) = { 0s } |
39 | 38 | rexeqi 3316 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈ ( L
‘ 1s )𝑎 =
(((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑞 ∈ { 0s }𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))) |
40 | | 0sno 27674 |
. . . . . . . . . . . . 13
⊢
0s ∈ No |
41 | 40 | elexi 3486 |
. . . . . . . . . . . 12
⊢
0s ∈ V |
42 | | oveq2 7409 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 0s → (𝑥 ·s 𝑞) = (𝑥 ·s 0s
)) |
43 | 42 | oveq2d 7417 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 0s → ((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) = ((𝑝 ·s 1s )
+s (𝑥
·s 0s ))) |
44 | | oveq2 7409 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 0s → (𝑝 ·s 𝑞) = (𝑝 ·s 0s
)) |
45 | 43, 44 | oveq12d 7419 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 0s → (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s
))) |
46 | 45 | eqeq2d 2735 |
. . . . . . . . . . . 12
⊢ (𝑞 = 0s → (𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))
↔ 𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 0s ))
-s (𝑝
·s 0s )))) |
47 | 41, 46 | rexsn 4678 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈ {
0s }𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s
))) |
48 | 39, 47 | bitri 275 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈ ( L
‘ 1s )𝑎 =
(((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ 𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s
))) |
49 | 48 | rexbii 3086 |
. . . . . . . . 9
⊢
(∃𝑝 ∈ ( L
‘𝑥)∃𝑞 ∈ ( L ‘
1s )𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s
))) |
50 | | risset 3222 |
. . . . . . . . 9
⊢ (𝑎 ∈ ( L ‘𝑥) ↔ ∃𝑝 ∈ ( L ‘𝑥)𝑝 = 𝑎) |
51 | 37, 49, 50 | 3bitr4g 314 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))
↔ 𝑎 ∈ ( L
‘𝑥))) |
52 | 51 | eqabcdv 2860 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))} =
( L ‘𝑥)) |
53 | | rex0 4349 |
. . . . . . . . . . . 12
⊢ ¬
∃𝑠 ∈ ∅
𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠)) |
54 | | right1s 27737 |
. . . . . . . . . . . . 13
⊢ ( R
‘ 1s ) = ∅ |
55 | 54 | rexeqi 3316 |
. . . . . . . . . . . 12
⊢
(∃𝑠 ∈ ( R
‘ 1s )𝑏 =
(((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) ↔ ∃𝑠 ∈ ∅ 𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠))) |
56 | 53, 55 | mtbir 323 |
. . . . . . . . . . 11
⊢ ¬
∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) |
57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ( R ‘𝑥) → ¬ ∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))) |
58 | 57 | nrex 3066 |
. . . . . . . . 9
⊢ ¬
∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) |
59 | 58 | abf 4394 |
. . . . . . . 8
⊢ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘ 1s )𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠))} =
∅ |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝑥)∃𝑠 ∈ ( R ‘ 1s )𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠))} =
∅) |
61 | 52, 60 | uneq12d 4156 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = (( L ‘𝑥) ∪ ∅)) |
62 | | un0 4382 |
. . . . . 6
⊢ (( L
‘𝑥) ∪ ∅) =
( L ‘𝑥) |
63 | 61, 62 | eqtrdi 2780 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → ({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) = ( L ‘𝑥)) |
64 | | rex0 4349 |
. . . . . . . . . . . 12
⊢ ¬
∃𝑢 ∈ ∅
𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢)) |
65 | 54 | rexeqi 3316 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈ ( R
‘ 1s )𝑐 =
(((𝑡 ·s
1s ) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) ↔ ∃𝑢 ∈ ∅ 𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))) |
66 | 64, 65 | mtbir 323 |
. . . . . . . . . . 11
⊢ ¬
∃𝑢 ∈ ( R ‘
1s )𝑐 = (((𝑡 ·s
1s ) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) |
67 | 66 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ( L ‘𝑥) → ¬ ∃𝑢 ∈ ( R ‘
1s )𝑐 = (((𝑡 ·s
1s ) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢))) |
68 | 67 | nrex 3066 |
. . . . . . . . 9
⊢ ¬
∃𝑡 ∈ ( L
‘𝑥)∃𝑢 ∈ ( R ‘
1s )𝑐 = (((𝑡 ·s
1s ) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) |
69 | 68 | abf 4394 |
. . . . . . . 8
⊢ {𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))} =
∅ |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → {𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))} =
∅) |
71 | | elun2 4169 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ ( R ‘𝑥) → 𝑣 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) |
72 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s
1s ) = (𝑣
·s 1s )) |
73 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑣 → 𝑥𝑂 = 𝑣) |
74 | 72, 73 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s
1s ) = 𝑥𝑂 ↔ (𝑣 ·s
1s ) = 𝑣)) |
75 | 74 | rspcva 3602 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑣 ·s
1s ) = 𝑣) |
76 | 71, 75 | sylan 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ ( R ‘𝑥) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑣 ·s
1s ) = 𝑣) |
77 | 76 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂 ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 ·s 1s ) = 𝑣) |
78 | 77 | adantll 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 ·s 1s ) = 𝑣) |
79 | 20 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑥 ·s 0s ) =
0s ) |
80 | 78, 79 | oveq12d 7419 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → ((𝑣 ·s 1s )
+s (𝑥
·s 0s )) = (𝑣 +s 0s
)) |
81 | | rightssno 27723 |
. . . . . . . . . . . . . . . . . 18
⊢ ( R
‘𝑥) ⊆ No |
82 | 81 | sseli 3970 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ ( R ‘𝑥) → 𝑣 ∈ No
) |
83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → 𝑣 ∈ No
) |
84 | 83 | addsridd 27797 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 +s 0s ) = 𝑣) |
85 | 80, 84 | eqtrd 2764 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → ((𝑣 ·s 1s )
+s (𝑥
·s 0s )) = 𝑣) |
86 | | muls01 27927 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈
No → (𝑣
·s 0s ) = 0s ) |
87 | 83, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 ·s 0s ) =
0s ) |
88 | 85, 87 | oveq12d 7419 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s )) =
(𝑣 -s
0s )) |
89 | | subsid1 27891 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈
No → (𝑣
-s 0s ) = 𝑣) |
90 | 83, 89 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 -s 0s ) = 𝑣) |
91 | 88, 90 | eqtrd 2764 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s )) =
𝑣) |
92 | 91 | eqeq2d 2735 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s )) ↔
𝑑 = 𝑣)) |
93 | 38 | rexeqi 3316 |
. . . . . . . . . . . 12
⊢
(∃𝑤 ∈ ( L
‘ 1s )𝑑 =
(((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑤 ∈ { 0s }𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))) |
94 | | oveq2 7409 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 0s → (𝑥 ·s 𝑤) = (𝑥 ·s 0s
)) |
95 | 94 | oveq2d 7417 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 0s → ((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) = ((𝑣 ·s 1s )
+s (𝑥
·s 0s ))) |
96 | | oveq2 7409 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 0s → (𝑣 ·s 𝑤) = (𝑣 ·s 0s
)) |
97 | 95, 96 | oveq12d 7419 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 0s → (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s
))) |
98 | 97 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 0s → (𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))
↔ 𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 0s ))
-s (𝑣
·s 0s )))) |
99 | 41, 98 | rexsn 4678 |
. . . . . . . . . . . 12
⊢
(∃𝑤 ∈ {
0s }𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s
))) |
100 | 93, 99 | bitri 275 |
. . . . . . . . . . 11
⊢
(∃𝑤 ∈ ( L
‘ 1s )𝑑 =
(((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s
))) |
101 | | equcom 2013 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑑 ↔ 𝑑 = 𝑣) |
102 | 92, 100, 101 | 3bitr4g 314 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ 𝑣 = 𝑑)) |
103 | 102 | rexbidva 3168 |
. . . . . . . . 9
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘ 1s )𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))
↔ ∃𝑣 ∈ ( R
‘𝑥)𝑣 = 𝑑)) |
104 | | risset 3222 |
. . . . . . . . 9
⊢ (𝑑 ∈ ( R ‘𝑥) ↔ ∃𝑣 ∈ ( R ‘𝑥)𝑣 = 𝑑) |
105 | 103, 104 | bitr4di 289 |
. . . . . . . 8
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘ 1s )𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))
↔ 𝑑 ∈ ( R
‘𝑥))) |
106 | 105 | eqabcdv 2860 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘ 1s )𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))} =
( R ‘𝑥)) |
107 | 70, 106 | uneq12d 4156 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = (∅ ∪ ( R ‘𝑥))) |
108 | | 0un 4384 |
. . . . . 6
⊢ (∅
∪ ( R ‘𝑥)) = ( R
‘𝑥) |
109 | 107, 108 | eqtrdi 2780 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))}) = ( R ‘𝑥)) |
110 | 63, 109 | oveq12d 7419 |
. . . 4
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (({𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))}
∪ {𝑏 ∣
∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) |s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝑥)∃𝑢 ∈ ( R ‘ 1s )𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢))}
∪ {𝑑 ∣
∃𝑣 ∈ ( R
‘𝑥)∃𝑤 ∈ ( L ‘
1s )𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤))})) = (( L ‘𝑥) |s ( R ‘𝑥))) |
111 | | lrcut 27744 |
. . . . 5
⊢ (𝑥 ∈
No → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥) |
112 | 111 | adantr 480 |
. . . 4
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (( L
‘𝑥) |s ( R
‘𝑥)) = 𝑥) |
113 | 10, 110, 112 | 3eqtrd 2768 |
. . 3
⊢ ((𝑥 ∈
No ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (𝑥 ·s
1s ) = 𝑥) |
114 | 113 | ex 412 |
. 2
⊢ (𝑥 ∈
No → (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂 → (𝑥 ·s
1s ) = 𝑥)) |
115 | 3, 6, 114 | noinds 27777 |
1
⊢ (𝐴 ∈
No → (𝐴
·s 1s ) = 𝐴) |