Theorem mulsfn

Description: Surreal multiplication is a function over surreals. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	mulsfn	⊢ ·s Fn ( No × No )

Proof

Step	Hyp	Ref	Expression
1		df-muls	⊢ ·s = norec2 ( ( 𝑧 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) ) ) )
2	1	norec2fn	⊢ ·s Fn ( No × No )