Metamath Proof Explorer

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 )