Theorem mulsrid 28504

Description: Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)

Assertion

Ref	Expression
mulsrid	⊢ (𝐴 ∈ No → (𝐴 ·s 1s ) = 𝐴)

Proof of Theorem mulsrid

Dummy variables 𝑥 𝑥_𝑂 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑟 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7427	. . 3 ⊢ (𝑥 = 𝑥𝑂 → (𝑥 ·s 1s ) = (𝑥𝑂 ·s 1s ))
2		id 23	. . 3 ⊢ (𝑥 = 𝑥𝑂 → 𝑥 = 𝑥𝑂)
3	1, 2	eqeq12d 2776	. 2 ⊢ (𝑥 = 𝑥𝑂 → ((𝑥 ·s 1s ) = 𝑥 ↔ (𝑥𝑂 ·s 1s ) = 𝑥𝑂))
4		oveq1 7427	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ·s 1s ) = (𝐴 ·s 1s ))
5		id 23	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
6	4, 5	eqeq12d 2776	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ·s 1s ) = 𝑥 ↔ (𝐴 ·s 1s ) = 𝐴))
7		1no 28201	. . . . . 6 ⊢ 1s ∈ No
8		mulsval 28500	. . . . . 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 704	. . . . 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 486	. . . 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 4180	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ (L‘𝑥) → 𝑝 ∈ ((L‘𝑥) ∪ (R‘𝑥)))
12		oveq1 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑝 → (𝑥𝑂 ·s 1s ) = (𝑝 ·s 1s ))
13		id 23	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑝 → 𝑥𝑂 = 𝑝)
14	12, 13	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑝 → ((𝑥𝑂 ·s 1s ) = 𝑥𝑂 ↔ (𝑝 ·s 1s ) = 𝑝))
15	14	rspcva 3574	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ ((L‘𝑥) ∪ (R‘𝑥)) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (𝑝 ·s 1s ) = 𝑝)
16	11, 15	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ (L‘𝑥) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (𝑝 ·s 1s ) = 𝑝)
17	16	ancoms 464	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂 ∧ 𝑝 ∈ (L‘𝑥)) → (𝑝 ·s 1s ) = 𝑝)
18	17	adantll 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑝 ·s 1s ) = 𝑝)
19		muls01 28503	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ No → (𝑥 ·s 0s ) = 0s )
20	19	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (𝑥 ·s 0s ) = 0s )
21	20	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑥 ·s 0s ) = 0s )
22	18, 21	oveq12d 7438	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → ((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) = (𝑝 +s 0s ))
23		leftno 28268	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (L‘𝑥) → 𝑝 ∈ No)
24	23	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → 𝑝 ∈ No)
25	24	addsridd 28356	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑝 +s 0s ) = 𝑝)
26	22, 25	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → ((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) = 𝑝)
27		muls01 28503	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ No → (𝑝 ·s 0s ) = 0s )
28	24, 27	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑝 ·s 0s ) = 0s )
29	26, 28	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )) = (𝑝 −s 0s ))
30		subsid1 28459	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ No → (𝑝 −s 0s ) = 𝑝)
31	24, 30	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑝 −s 0s ) = 𝑝)
32	29, 31	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )) = 𝑝)
33	32	eqeq2d 2771	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )) ↔ 𝑎 = 𝑝))
34		equcom 2050	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑝 ↔ 𝑝 = 𝑎)
35	33, 34	bitrdi 290	. . . . . . . . . 10 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑝 ∈ (L‘𝑥)) → (𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )) ↔ 𝑝 = 𝑎))
36	35	rexbidva 3184	. . . . . . . . 9 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (∃𝑝 ∈ (L‘𝑥)𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )) ↔ ∃𝑝 ∈ (L‘𝑥)𝑝 = 𝑎))
37		left1s 28286	. . . . . . . . . . . 12 ⊢ (L‘ 1s ) = { 0s }
38	37	rexeqi 3318	. . . . . . . . . . 11 ⊢ (∃𝑞 ∈ (L‘ 1s )𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ ∃𝑞 ∈ { 0s }𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)))
39		0no 28200	. . . . . . . . . . . . 13 ⊢ 0s ∈ No
40	39	elexi 3472	. . . . . . . . . . . 12 ⊢ 0s ∈ V
41		oveq2 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 0s → (𝑥 ·s 𝑞) = (𝑥 ·s 0s ))
42	41	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 0s → ((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) = ((𝑝 ·s 1s ) +s (𝑥 ·s 0s )))
43		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 0s → (𝑝 ·s 𝑞) = (𝑝 ·s 0s ))
44	42, 43	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝑞 = 0s → (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )))
45	44	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑞 = 0s → (𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ 𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s ))))
46	40, 45	rexsn 4639	. . . . . . . . . . 11 ⊢ (∃𝑞 ∈ { 0s }𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ 𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )))
47	38, 46	bitri 278	. . . . . . . . . 10 ⊢ (∃𝑞 ∈ (L‘ 1s )𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ 𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )))
48	47	rexbii 3109	. . . . . . . . 9 ⊢ (∃𝑝 ∈ (L‘𝑥)∃𝑞 ∈ (L‘ 1s )𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ ∃𝑝 ∈ (L‘𝑥)𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑝 ·s 0s )))
49		risset 3237	. . . . . . . . 9 ⊢ (𝑎 ∈ (L‘𝑥) ↔ ∃𝑝 ∈ (L‘𝑥)𝑝 = 𝑎)
50	36, 48, 49	3bitr4g 317	. . . . . . . 8 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (∃𝑝 ∈ (L‘𝑥)∃𝑞 ∈ (L‘ 1s )𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞)) ↔ 𝑎 ∈ (L‘𝑥)))
51	50	eqabcdv 2894	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → {𝑎 ∣ ∃𝑝 ∈ (L‘𝑥)∃𝑞 ∈ (L‘ 1s )𝑎 = (((𝑝 ·s 1s ) +s (𝑥 ·s 𝑞)) −s (𝑝 ·s 𝑞))} = (L‘𝑥))
52		rex0 4307	. . . . . . . . . . . 12 ⊢ ¬ ∃𝑠 ∈ ∅ 𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠))
53		right1s 28287	. . . . . . . . . . . . 13 ⊢ (R‘ 1s ) = ∅
54	53	rexeqi 3318	. . . . . . . . . . . 12 ⊢ (∃𝑠 ∈ (R‘ 1s )𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠)) ↔ ∃𝑠 ∈ ∅ 𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠)))
55	52, 54	mtbir 326	. . . . . . . . . . 11 ⊢ ¬ ∃𝑠 ∈ (R‘ 1s )𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠))
56	55	a1i 11	. . . . . . . . . 10 ⊢ (𝑟 ∈ (R‘𝑥) → ¬ ∃𝑠 ∈ (R‘ 1s )𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠)))
57	56	nrex 3090	. . . . . . . . 9 ⊢ ¬ ∃𝑟 ∈ (R‘𝑥)∃𝑠 ∈ (R‘ 1s )𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠))
58	57	abf 4363	. . . . . . . 8 ⊢ {𝑏 ∣ ∃𝑟 ∈ (R‘𝑥)∃𝑠 ∈ (R‘ 1s )𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠))} = ∅
59	58	a1i 11	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → {𝑏 ∣ ∃𝑟 ∈ (R‘𝑥)∃𝑠 ∈ (R‘ 1s )𝑏 = (((𝑟 ·s 1s ) +s (𝑥 ·s 𝑠)) −s (𝑟 ·s 𝑠))} = ∅)
60	51, 59	uneq12d 4168	. . . . . 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‘𝑥) ∪ ∅))
61		un0 4343	. . . . . 6 ⊢ ((L‘𝑥) ∪ ∅) = (L‘𝑥)
62	60, 61	eqtrdi 2811	. . . . 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‘𝑥))
63		rex0 4307	. . . . . . . . . . . 12 ⊢ ¬ ∃𝑢 ∈ ∅ 𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢))
64	53	rexeqi 3318	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ (R‘ 1s )𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢)) ↔ ∃𝑢 ∈ ∅ 𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢)))
65	63, 64	mtbir 326	. . . . . . . . . . 11 ⊢ ¬ ∃𝑢 ∈ (R‘ 1s )𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢))
66	65	a1i 11	. . . . . . . . . 10 ⊢ (𝑡 ∈ (L‘𝑥) → ¬ ∃𝑢 ∈ (R‘ 1s )𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢)))
67	66	nrex 3090	. . . . . . . . 9 ⊢ ¬ ∃𝑡 ∈ (L‘𝑥)∃𝑢 ∈ (R‘ 1s )𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢))
68	67	abf 4363	. . . . . . . 8 ⊢ {𝑐 ∣ ∃𝑡 ∈ (L‘𝑥)∃𝑢 ∈ (R‘ 1s )𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢))} = ∅
69	68	a1i 11	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → {𝑐 ∣ ∃𝑡 ∈ (L‘𝑥)∃𝑢 ∈ (R‘ 1s )𝑐 = (((𝑡 ·s 1s ) +s (𝑥 ·s 𝑢)) −s (𝑡 ·s 𝑢))} = ∅)
70		elun2 4181	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ (R‘𝑥) → 𝑣 ∈ ((L‘𝑥) ∪ (R‘𝑥)))
71		oveq1 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑣 → (𝑥𝑂 ·s 1s ) = (𝑣 ·s 1s ))
72		id 23	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑣 → 𝑥𝑂 = 𝑣)
73	71, 72	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑣 → ((𝑥𝑂 ·s 1s ) = 𝑥𝑂 ↔ (𝑣 ·s 1s ) = 𝑣))
74	73	rspcva 3574	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑣 ∈ ((L‘𝑥) ∪ (R‘𝑥)) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (𝑣 ·s 1s ) = 𝑣)
75	70, 74	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ (R‘𝑥) ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (𝑣 ·s 1s ) = 𝑣)
76	75	ancoms 464	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂 ∧ 𝑣 ∈ (R‘𝑥)) → (𝑣 ·s 1s ) = 𝑣)
77	76	adantll 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (𝑣 ·s 1s ) = 𝑣)
78	20	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (𝑥 ·s 0s ) = 0s )
79	77, 78	oveq12d 7438	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → ((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) = (𝑣 +s 0s ))
80		rightno 28269	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ (R‘𝑥) → 𝑣 ∈ No)
81	80	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → 𝑣 ∈ No)
82	81	addsridd 28356	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (𝑣 +s 0s ) = 𝑣)
83	79, 82	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → ((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) = 𝑣)
84		muls01 28503	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ No → (𝑣 ·s 0s ) = 0s )
85	81, 84	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (𝑣 ·s 0s ) = 0s )
86	83, 85	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s )) = (𝑣 −s 0s ))
87		subsid1 28459	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ No → (𝑣 −s 0s ) = 𝑣)
88	81, 87	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (𝑣 −s 0s ) = 𝑣)
89	86, 88	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s )) = 𝑣)
90	89	eqeq2d 2771	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s )) ↔ 𝑑 = 𝑣))
91	37	rexeqi 3318	. . . . . . . . . . . 12 ⊢ (∃𝑤 ∈ (L‘ 1s )𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ ∃𝑤 ∈ { 0s }𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)))
92		oveq2 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 0s → (𝑥 ·s 𝑤) = (𝑥 ·s 0s ))
93	92	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 0s → ((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) = ((𝑣 ·s 1s ) +s (𝑥 ·s 0s )))
94		oveq2 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 0s → (𝑣 ·s 𝑤) = (𝑣 ·s 0s ))
95	93, 94	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 0s → (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) = (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s )))
96	95	eqeq2d 2771	. . . . . . . . . . . . 13 ⊢ (𝑤 = 0s → (𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ 𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s ))))
97	40, 96	rexsn 4639	. . . . . . . . . . . 12 ⊢ (∃𝑤 ∈ { 0s }𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ 𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s )))
98	91, 97	bitri 278	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ (L‘ 1s )𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ 𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 0s )) −s (𝑣 ·s 0s )))
99		equcom 2050	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑑 ↔ 𝑑 = 𝑣)
100	90, 98, 99	3bitr4g 317	. . . . . . . . . 10 ⊢ (((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) ∧ 𝑣 ∈ (R‘𝑥)) → (∃𝑤 ∈ (L‘ 1s )𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ 𝑣 = 𝑑))
101	100	rexbidva 3184	. . . . . . . . 9 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (∃𝑣 ∈ (R‘𝑥)∃𝑤 ∈ (L‘ 1s )𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ ∃𝑣 ∈ (R‘𝑥)𝑣 = 𝑑))
102		risset 3237	. . . . . . . . 9 ⊢ (𝑑 ∈ (R‘𝑥) ↔ ∃𝑣 ∈ (R‘𝑥)𝑣 = 𝑑)
103	101, 102	bitr4di 292	. . . . . . . 8 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (∃𝑣 ∈ (R‘𝑥)∃𝑤 ∈ (L‘ 1s )𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤)) ↔ 𝑑 ∈ (R‘𝑥)))
104	103	eqabcdv 2894	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → {𝑑 ∣ ∃𝑣 ∈ (R‘𝑥)∃𝑤 ∈ (L‘ 1s )𝑑 = (((𝑣 ·s 1s ) +s (𝑥 ·s 𝑤)) −s (𝑣 ·s 𝑤))} = (R‘𝑥))
105	69, 104	uneq12d 4168	. . . . . 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‘𝑥)))
106		0un 4345	. . . . . 6 ⊢ (∅ ∪ (R‘𝑥)) = (R‘𝑥)
107	105, 106	eqtrdi 2811	. . . . 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‘𝑥))
108	62, 107	oveq12d 7438	. . . 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‘𝑥)))
109		lrcut 28295	. . . . 5 ⊢ (𝑥 ∈ No → ((L‘𝑥) |s (R‘𝑥)) = 𝑥)
110	109	adantr 486	. . . 4 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → ((L‘𝑥) |s (R‘𝑥)) = 𝑥)
111	10, 108, 110	3eqtrd 2799	. . 3 ⊢ ((𝑥 ∈ No ∧ ∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂) → (𝑥 ·s 1s ) = 𝑥)
112	111	ex 418	. 2 ⊢ (𝑥 ∈ No → (∀𝑥𝑂 ∈ ((L‘𝑥) ∪ (R‘𝑥))(𝑥𝑂 ·s 1s ) = 𝑥𝑂 → (𝑥 ·s 1s ) = 𝑥))
113	3, 6, 112	noinds 28336	1 ⊢ (𝐴 ∈ No → (𝐴 ·s 1s ) = 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086   ∪ cun 4149  ∅c0 4278  {csn 4584  ‘cfv 6538  (class class class)co 7420  Nocsur 28002   |s ccuts 28150   0_s c0s 28196   1_s c1s 28197  Lcleft 28216  Rcright 28217   +_s cadds 28350   −_s csubs 28411   ·_s cmuls 28497

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-1o 8479  df-2o 8480  df-no 28005  df-lts 28006  df-bday 28007  df-les 28107  df-slts 28149  df-cuts 28151  df-0s 28198  df-1s 28199  df-made 28218  df-old 28219  df-left 28221  df-right 28222  df-norec 28329  df-norec2 28340  df-adds 28351  df-negs 28412  df-subs 28413  df-muls 28498

This theorem is used by:  mulsridd  28505  mulslid  28533  n0seo  28812  zseo  28813  pw2recs  28829  addhalfcut  28850  pw2cutp1  28852  bdaypw2n0bndlem  28854  bdayfinbndlem1  28858  remulscllem1  28891