Theorem mulsunif

Description: Surreal multiplication has the uniformity property. That is, any cuts that define A and B can be used in the definition of ( A x.s B ) . Theorem 3.5 of Gonshor p. 18. (Contributed by Scott Fenton, 7-Mar-2025)

	Ref	Expression
Hypotheses	mulsunif.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
	mulsunif.2	⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
	mulsunif.3	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
	mulsunif.4	⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
Assertion	mulsunif	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulsunif.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2		mulsunif.2	⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3		mulsunif.3	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
4		mulsunif.4	⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
5	1 2 3 4	mulsuniflem	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑒 ∣ ∃ 𝑓 ∈ 𝐿 ∃ 𝑔 ∈ 𝑀 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) } ∪ { ℎ ∣ ∃ 𝑖 ∈ 𝑅 ∃ 𝑗 ∈ 𝑆 ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑗 ) ) -s ( 𝑖 ·s 𝑗 ) ) } ) |s ( { 𝑘 ∣ ∃ 𝑙 ∈ 𝐿 ∃ 𝑚 ∈ 𝑆 𝑘 = ( ( ( 𝑙 ·s 𝐵 ) +s ( 𝐴 ·s 𝑚 ) ) -s ( 𝑙 ·s 𝑚 ) ) } ∪ { 𝑛 ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 𝑛 = ( ( ( 𝑜 ·s 𝐵 ) +s ( 𝐴 ·s 𝑥 ) ) -s ( 𝑜 ·s 𝑥 ) ) } ) ) )
6		mulsval2lem	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = { 𝑒 ∣ ∃ 𝑓 ∈ 𝐿 ∃ 𝑔 ∈ 𝑀 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) }
7		mulsval2lem	⊢ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } = { ℎ ∣ ∃ 𝑖 ∈ 𝑅 ∃ 𝑗 ∈ 𝑆 ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑗 ) ) -s ( 𝑖 ·s 𝑗 ) ) }
8	6 7	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) = ( { 𝑒 ∣ ∃ 𝑓 ∈ 𝐿 ∃ 𝑔 ∈ 𝑀 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) } ∪ { ℎ ∣ ∃ 𝑖 ∈ 𝑅 ∃ 𝑗 ∈ 𝑆 ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑗 ) ) -s ( 𝑖 ·s 𝑗 ) ) } )
9		mulsval2lem	⊢ { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } = { 𝑘 ∣ ∃ 𝑙 ∈ 𝐿 ∃ 𝑚 ∈ 𝑆 𝑘 = ( ( ( 𝑙 ·s 𝐵 ) +s ( 𝐴 ·s 𝑚 ) ) -s ( 𝑙 ·s 𝑚 ) ) }
10		mulsval2lem	⊢ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } = { 𝑛 ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 𝑛 = ( ( ( 𝑜 ·s 𝐵 ) +s ( 𝐴 ·s 𝑥 ) ) -s ( 𝑜 ·s 𝑥 ) ) }
11	9 10	uneq12i	⊢ ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) = ( { 𝑘 ∣ ∃ 𝑙 ∈ 𝐿 ∃ 𝑚 ∈ 𝑆 𝑘 = ( ( ( 𝑙 ·s 𝐵 ) +s ( 𝐴 ·s 𝑚 ) ) -s ( 𝑙 ·s 𝑚 ) ) } ∪ { 𝑛 ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 𝑛 = ( ( ( 𝑜 ·s 𝐵 ) +s ( 𝐴 ·s 𝑥 ) ) -s ( 𝑜 ·s 𝑥 ) ) } )
12	8 11	oveq12i	⊢ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) = ( ( { 𝑒 ∣ ∃ 𝑓 ∈ 𝐿 ∃ 𝑔 ∈ 𝑀 𝑒 = ( ( ( 𝑓 ·s 𝐵 ) +s ( 𝐴 ·s 𝑔 ) ) -s ( 𝑓 ·s 𝑔 ) ) } ∪ { ℎ ∣ ∃ 𝑖 ∈ 𝑅 ∃ 𝑗 ∈ 𝑆 ℎ = ( ( ( 𝑖 ·s 𝐵 ) +s ( 𝐴 ·s 𝑗 ) ) -s ( 𝑖 ·s 𝑗 ) ) } ) |s ( { 𝑘 ∣ ∃ 𝑙 ∈ 𝐿 ∃ 𝑚 ∈ 𝑆 𝑘 = ( ( ( 𝑙 ·s 𝐵 ) +s ( 𝐴 ·s 𝑚 ) ) -s ( 𝑙 ·s 𝑚 ) ) } ∪ { 𝑛 ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 𝑛 = ( ( ( 𝑜 ·s 𝐵 ) +s ( 𝐴 ·s 𝑥 ) ) -s ( 𝑜 ·s 𝑥 ) ) } ) )
13	5 12	eqtr4di	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )