Theorem muls01

Description: Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	muls01	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		0sno	⊢ 0s ∈ No
2		mulsval	⊢ ( ( 𝐴 ∈ 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	⊢ ( 𝐴 ∈ 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	⊢ ¬ ∃ 𝑞 ∈ ∅ 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) )
5		left0s	⊢ ( L ‘ 0s ) = ∅
6	5	rexeqi	⊢ ( ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑞 ∈ ∅ 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
7	4 6	mtbir	⊢ ¬ ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) )
8	7	a1i	⊢ ( 𝑝 ∈ ( L ‘ 𝐴 ) → ¬ ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
9	8	nrex	⊢ ¬ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) )
10	9	abf	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = ∅
11		rex0	⊢ ¬ ∃ 𝑠 ∈ ∅ 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) )
12		right0s	⊢ ( R ‘ 0s ) = ∅
13	12	rexeqi	⊢ ( ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ ∃ 𝑠 ∈ ∅ 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
14	11 13	mtbir	⊢ ¬ ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) )
15	14	a1i	⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) → ¬ ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
16	15	nrex	⊢ ¬ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) )
17	16	abf	⊢ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } = ∅
18	10 17	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) = ( ∅ ∪ ∅ )
19		un0	⊢ ( ∅ ∪ ∅ ) = ∅
20	18 19	eqtri	⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 0s ) 𝑎 = ( ( ( 𝑝 ·s 0s ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 0s ) 𝑏 = ( ( ( 𝑟 ·s 0s ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) = ∅
21		rex0	⊢ ¬ ∃ 𝑢 ∈ ∅ 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) )
22	12	rexeqi	⊢ ( ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ ∃ 𝑢 ∈ ∅ 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
23	21 22	mtbir	⊢ ¬ ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) )
24	23	a1i	⊢ ( 𝑡 ∈ ( L ‘ 𝐴 ) → ¬ ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
25	24	nrex	⊢ ¬ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) )
26	25	abf	⊢ { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } = ∅
27		rex0	⊢ ¬ ∃ 𝑤 ∈ ∅ 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) )
28	5	rexeqi	⊢ ( ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ∃ 𝑤 ∈ ∅ 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
29	27 28	mtbir	⊢ ¬ ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) )
30	29	a1i	⊢ ( 𝑣 ∈ ( R ‘ 𝐴 ) → ¬ ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
31	30	nrex	⊢ ¬ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) )
32	31	abf	⊢ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } = ∅
33	26 32	uneq12i	⊢ ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) = ( ∅ ∪ ∅ )
34	33 19	eqtri	⊢ ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 0s ) 𝑐 = ( ( ( 𝑡 ·s 0s ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 0s ) 𝑑 = ( ( ( 𝑣 ·s 0s ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) = ∅
35	20 34	oveq12i	⊢ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( 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	⊢ 0s = ( ∅ |s ∅ )
37	35 36	eqtr4i	⊢ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( 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	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )