| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . 3
⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s
1s ) = (𝑥𝑂 ·s
1s )) | 
| 2 |  | id 22 | . . 3
⊢ (𝑥 = 𝑥𝑂 → 𝑥 = 𝑥𝑂) | 
| 3 | 1, 2 | eqeq12d 2753 | . 2
⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s
1s ) = 𝑥 ↔
(𝑥𝑂
·s 1s ) = 𝑥𝑂)) | 
| 4 |  | oveq1 7438 | . . 3
⊢ (𝑥 = 𝐴 → (𝑥 ·s 1s ) =
(𝐴 ·s
1s )) | 
| 5 |  | id 22 | . . 3
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | 
| 6 | 4, 5 | eqeq12d 2753 | . 2
⊢ (𝑥 = 𝐴 → ((𝑥 ·s 1s ) = 𝑥 ↔ (𝐴 ·s 1s ) =
𝐴)) | 
| 7 |  | 1sno 27872 | . . . . . 6
⊢ 
1s ∈  No | 
| 8 |  | mulsval 28135 | . . . . . 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 691 | . . . . 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 4182 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ ( L ‘𝑥) → 𝑝 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) | 
| 12 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s
1s ) = (𝑝
·s 1s )) | 
| 13 |  | id 22 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑝 → 𝑥𝑂 = 𝑝) | 
| 14 | 12, 13 | eqeq12d 2753 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s
1s ) = 𝑥𝑂 ↔ (𝑝 ·s
1s ) = 𝑝)) | 
| 15 | 14 | rspcva 3620 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑝 ·s
1s ) = 𝑝) | 
| 16 | 11, 15 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ( L ‘𝑥) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑝 ·s
1s ) = 𝑝) | 
| 17 | 16 | ancoms 458 | . . . . . . . . . . . . . . . . 17
⊢
((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂 ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 ·s 1s ) = 𝑝) | 
| 18 | 17 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 ·s 1s ) = 𝑝) | 
| 19 |  | muls01 28138 | . . . . . . . . . . . . . . . . . 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 7449 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → ((𝑝 ·s 1s )
+s (𝑥
·s 0s )) = (𝑝 +s 0s
)) | 
| 23 |  | leftssno 27919 | . . . . . . . . . . . . . . . . . 18
⊢ ( L
‘𝑥) ⊆  No | 
| 24 | 23 | sseli 3979 | . . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ( L ‘𝑥) → 𝑝 ∈  No
) | 
| 25 | 24 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → 𝑝 ∈  No
) | 
| 26 | 25 | addsridd 27998 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 +s 0s ) = 𝑝) | 
| 27 | 22, 26 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → ((𝑝 ·s 1s )
+s (𝑥
·s 0s )) = 𝑝) | 
| 28 |  | muls01 28138 | . . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ 
No  → (𝑝
·s 0s ) = 0s ) | 
| 29 | 25, 28 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 ·s 0s ) =
0s ) | 
| 30 | 27, 29 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) =
(𝑝 -s
0s )) | 
| 31 |  | subsid1 28098 | . . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 
No  → (𝑝
-s 0s ) = 𝑝) | 
| 32 | 25, 31 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑝 -s 0s ) = 𝑝) | 
| 33 | 30, 32 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) =
𝑝) | 
| 34 | 33 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) ↔
𝑎 = 𝑝)) | 
| 35 |  | equcom 2017 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑝 ↔ 𝑝 = 𝑎) | 
| 36 | 34, 35 | bitrdi 287 | . . . . . . . . . 10
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑝 ∈ ( L ‘𝑥)) → (𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) ↔
𝑝 = 𝑎)) | 
| 37 | 36 | rexbidva 3177 | . . . . . . . . 9
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s )) ↔
∃𝑝 ∈ ( L
‘𝑥)𝑝 = 𝑎)) | 
| 38 |  | left1s 27933 | . . . . . . . . . . . 12
⊢ ( L
‘ 1s ) = { 0s } | 
| 39 | 38 | rexeqi 3325 | . . . . . . . . . . 11
⊢
(∃𝑞 ∈ ( L
‘ 1s )𝑎 =
(((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑞 ∈ { 0s }𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))) | 
| 40 |  | 0sno 27871 | . . . . . . . . . . . . 13
⊢ 
0s ∈  No | 
| 41 | 40 | elexi 3503 | . . . . . . . . . . . 12
⊢ 
0s ∈ V | 
| 42 |  | oveq2 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑞 = 0s → (𝑥 ·s 𝑞) = (𝑥 ·s 0s
)) | 
| 43 | 42 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑞 = 0s → ((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) = ((𝑝 ·s 1s )
+s (𝑥
·s 0s ))) | 
| 44 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑞 = 0s → (𝑝 ·s 𝑞) = (𝑝 ·s 0s
)) | 
| 45 | 43, 44 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑞 = 0s → (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s
))) | 
| 46 | 45 | eqeq2d 2748 | . . . . . . . . . . . 12
⊢ (𝑞 = 0s → (𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))
↔ 𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 0s ))
-s (𝑝
·s 0s )))) | 
| 47 | 41, 46 | rexsn 4682 | . . . . . . . . . . 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 3094 | . . . . . . . . 9
⊢
(∃𝑝 ∈ ( L
‘𝑥)∃𝑞 ∈ ( L ‘
1s )𝑎 = (((𝑝 ·s
1s ) +s (𝑥 ·s 𝑞)) -s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ ( L ‘𝑥)𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑝 ·s 0s
))) | 
| 50 |  | risset 3233 | . . . . . . . . 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 2876 | . . . . . . 7
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → {𝑎 ∣ ∃𝑝 ∈ ( L ‘𝑥)∃𝑞 ∈ ( L ‘ 1s )𝑎 = (((𝑝 ·s 1s )
+s (𝑥
·s 𝑞))
-s (𝑝
·s 𝑞))} =
( L ‘𝑥)) | 
| 53 |  | rex0 4360 | . . . . . . . . . . . 12
⊢  ¬
∃𝑠 ∈ ∅
𝑏 = (((𝑟 ·s 1s )
+s (𝑥
·s 𝑠))
-s (𝑟
·s 𝑠)) | 
| 54 |  | right1s 27934 | . . . . . . . . . . . . 13
⊢ ( R
‘ 1s ) = ∅ | 
| 55 | 54 | rexeqi 3325 | . . . . . . . . . . . 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 3074 | . . . . . . . . 9
⊢  ¬
∃𝑟 ∈ ( R
‘𝑥)∃𝑠 ∈ ( R ‘
1s )𝑏 = (((𝑟 ·s
1s ) +s (𝑥 ·s 𝑠)) -s (𝑟 ·s 𝑠)) | 
| 59 | 58 | abf 4406 | . . . . . . . 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 4169 | . . . . . 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 4394 | . . . . . 6
⊢ (( L
‘𝑥) ∪ ∅) =
( L ‘𝑥) | 
| 63 | 61, 62 | eqtrdi 2793 | . . . . 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 4360 | . . . . . . . . . . . 12
⊢  ¬
∃𝑢 ∈ ∅
𝑐 = (((𝑡 ·s 1s )
+s (𝑥
·s 𝑢))
-s (𝑡
·s 𝑢)) | 
| 65 | 54 | rexeqi 3325 | . . . . . . . . . . . 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 3074 | . . . . . . . . 9
⊢  ¬
∃𝑡 ∈ ( L
‘𝑥)∃𝑢 ∈ ( R ‘
1s )𝑐 = (((𝑡 ·s
1s ) +s (𝑥 ·s 𝑢)) -s (𝑡 ·s 𝑢)) | 
| 69 | 68 | abf 4406 | . . . . . . . 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 4183 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ ( R ‘𝑥) → 𝑣 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) | 
| 72 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s
1s ) = (𝑣
·s 1s )) | 
| 73 |  | id 22 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑣 → 𝑥𝑂 = 𝑣) | 
| 74 | 72, 73 | eqeq12d 2753 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s
1s ) = 𝑥𝑂 ↔ (𝑣 ·s
1s ) = 𝑣)) | 
| 75 | 74 | rspcva 3620 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑣 ·s
1s ) = 𝑣) | 
| 76 | 71, 75 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ ( R ‘𝑥) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))(𝑥𝑂
·s 1s ) = 𝑥𝑂) → (𝑣 ·s
1s ) = 𝑣) | 
| 77 | 76 | ancoms 458 | . . . . . . . . . . . . . . . . 17
⊢
((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂 ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 ·s 1s ) = 𝑣) | 
| 78 | 77 | adantll 714 | . . . . . . . . . . . . . . . 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 7449 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → ((𝑣 ·s 1s )
+s (𝑥
·s 0s )) = (𝑣 +s 0s
)) | 
| 81 |  | rightssno 27920 | . . . . . . . . . . . . . . . . . 18
⊢ ( R
‘𝑥) ⊆  No | 
| 82 | 81 | sseli 3979 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ ( R ‘𝑥) → 𝑣 ∈  No
) | 
| 83 | 82 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → 𝑣 ∈  No
) | 
| 84 | 83 | addsridd 27998 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 +s 0s ) = 𝑣) | 
| 85 | 80, 84 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → ((𝑣 ·s 1s )
+s (𝑥
·s 0s )) = 𝑣) | 
| 86 |  | muls01 28138 | . . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 
No  → (𝑣
·s 0s ) = 0s ) | 
| 87 | 83, 86 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 ·s 0s ) =
0s ) | 
| 88 | 85, 87 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s )) =
(𝑣 -s
0s )) | 
| 89 |  | subsid1 28098 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 
No  → (𝑣
-s 0s ) = 𝑣) | 
| 90 | 83, 89 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑣 -s 0s ) = 𝑣) | 
| 91 | 88, 90 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s )) =
𝑣) | 
| 92 | 91 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) ∧ 𝑣 ∈ ( R ‘𝑥)) → (𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s )) ↔
𝑑 = 𝑣)) | 
| 93 | 38 | rexeqi 3325 | . . . . . . . . . . . 12
⊢
(∃𝑤 ∈ ( L
‘ 1s )𝑑 =
(((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) ↔ ∃𝑤 ∈ { 0s }𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))) | 
| 94 |  | oveq2 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 0s → (𝑥 ·s 𝑤) = (𝑥 ·s 0s
)) | 
| 95 | 94 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 0s → ((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) = ((𝑣 ·s 1s )
+s (𝑥
·s 0s ))) | 
| 96 |  | oveq2 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 0s → (𝑣 ·s 𝑤) = (𝑣 ·s 0s
)) | 
| 97 | 95, 96 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ (𝑤 = 0s → (((𝑣 ·s
1s ) +s (𝑥 ·s 𝑤)) -s (𝑣 ·s 𝑤)) = (((𝑣 ·s 1s )
+s (𝑥
·s 0s )) -s (𝑣 ·s 0s
))) | 
| 98 | 97 | eqeq2d 2748 | . . . . . . . . . . . . 13
⊢ (𝑤 = 0s → (𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))
↔ 𝑑 = (((𝑣 ·s
1s ) +s (𝑥 ·s 0s ))
-s (𝑣
·s 0s )))) | 
| 99 | 41, 98 | rexsn 4682 | . . . . . . . . . . . 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 2017 | . . . . . . . . . . 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 3177 | . . . . . . . . 9
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘ 1s )𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))
↔ ∃𝑣 ∈ ( R
‘𝑥)𝑣 = 𝑑)) | 
| 104 |  | risset 3233 | . . . . . . . . 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 2876 | . . . . . . 7
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝑥)∃𝑤 ∈ ( L ‘ 1s )𝑑 = (((𝑣 ·s 1s )
+s (𝑥
·s 𝑤))
-s (𝑣
·s 𝑤))} =
( R ‘𝑥)) | 
| 107 | 70, 106 | uneq12d 4169 | . . . . . 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 4396 | . . . . . 6
⊢ (∅
∪ ( R ‘𝑥)) = ( R
‘𝑥) | 
| 109 | 107, 108 | eqtrdi 2793 | . . . . 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 7449 | . . . 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 27941 | . . . . 5
⊢ (𝑥 ∈ 
No  → (( L ‘𝑥) |s ( R ‘𝑥)) = 𝑥) | 
| 112 | 111 | adantr 480 | . . . 4
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))(𝑥𝑂 ·s
1s ) = 𝑥𝑂) → (( L
‘𝑥) |s ( R
‘𝑥)) = 𝑥) | 
| 113 | 10, 110, 112 | 3eqtrd 2781 | . . 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 27978 | 1
⊢ (𝐴 ∈ 
No  → (𝐴
·s 1s ) = 𝐴) |