Theorem mulsval2

Description: The value of surreal multiplication, expressed with fewer distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

	Ref	Expression
Assertion	mulsval2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulsval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑒 ∣ ∃ 𝑓 ∈ ( L ‘ 𝐴 ) ∃ 𝑔 ∈ ( L ‘ 𝐵 ) 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) } ∪ { ℎ ∣ ∃ 𝑖 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑖 ·s 𝑘 ) ) } ) |s ( { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) } ∪ { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) } ) ) )
2		mulsval2lem	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = { 𝑒 ∣ ∃ 𝑓 ∈ ( L ‘ 𝐴 ) ∃ 𝑔 ∈ ( L ‘ 𝐵 ) 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) }
3		mulsval2lem	⊢ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } = { ℎ ∣ ∃ 𝑖 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑖 ·s 𝑘 ) ) }
4	2 3	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) = ( { 𝑒 ∣ ∃ 𝑓 ∈ ( L ‘ 𝐴 ) ∃ 𝑔 ∈ ( L ‘ 𝐵 ) 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) } ∪ { ℎ ∣ ∃ 𝑖 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑖 ·s 𝑘 ) ) } )
5		mulsval2lem	⊢ { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } = { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) }
6		mulsval2lem	⊢ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } = { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) }
7	5 6	uneq12i	⊢ ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) = ( { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) } ∪ { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) } )
8	4 7	oveq12i	⊢ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) = ( ( { 𝑒 ∣ ∃ 𝑓 ∈ ( L ‘ 𝐴 ) ∃ 𝑔 ∈ ( L ‘ 𝐵 ) 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) } ∪ { ℎ ∣ ∃ 𝑖 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑖 ·s 𝑘 ) ) } ) |s ( { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) } ∪ { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) } ) )
9	1 8	eqtr4di	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )