Theorem mulscut

Description: Show the cut properties of surreal multiplication. (Contributed by Scott Fenton, 8-Mar-2025)

	Ref	Expression
Hypotheses	mulscut.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulscut.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	mulscut	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -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		mulscut.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulscut.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	1 2	mulscutlem	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑓 ∣ ∃ 𝑔 ∈ ( L ‘ 𝐴 ) ∃ ℎ ∈ ( L ‘ 𝐵 ) 𝑓 = ( ( ( 𝑔 ·s 𝐵 ) +s ( 𝐴 ·s ℎ ) ) -s ( 𝑔 ·s ℎ ) ) } ∪ { 𝑖 ∣ ∃ 𝑗 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑗 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑗 ·s 𝑘 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) } ∪ { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) } ) ) )
4		biid	⊢ ( ( 𝐴 ·s 𝐵 ) ∈ No ↔ ( 𝐴 ·s 𝐵 ) ∈ No )
5		mulsval2lem	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = { 𝑓 ∣ ∃ 𝑔 ∈ ( L ‘ 𝐴 ) ∃ ℎ ∈ ( L ‘ 𝐵 ) 𝑓 = ( ( ( 𝑔 ·s 𝐵 ) +s ( 𝐴 ·s ℎ ) ) -s ( 𝑔 ·s ℎ ) ) }
6		mulsval2lem	⊢ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } = { 𝑖 ∣ ∃ 𝑗 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑗 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑗 ·s 𝑘 ) ) }
7	5 6	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 𝑘 ) ) } )
8	7	breq1i	⊢ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ↔ ( { 𝑓 ∣ ∃ 𝑔 ∈ ( L ‘ 𝐴 ) ∃ ℎ ∈ ( L ‘ 𝐵 ) 𝑓 = ( ( ( 𝑔 ·s 𝐵 ) +s ( 𝐴 ·s ℎ ) ) -s ( 𝑔 ·s ℎ ) ) } ∪ { 𝑖 ∣ ∃ 𝑗 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑗 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑗 ·s 𝑘 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } )
9		mulsval2lem	⊢ { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } = { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) }
10		mulsval2lem	⊢ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } = { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) }
11	9 10	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 𝑦 ) ) } )
12	11	breq2i	⊢ ( { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) } ∪ { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) } ) )
13	4 8 12	3anbi123i	⊢ ( ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑓 ∣ ∃ 𝑔 ∈ ( L ‘ 𝐴 ) ∃ ℎ ∈ ( L ‘ 𝐵 ) 𝑓 = ( ( ( 𝑔 ·s 𝐵 ) +s ( 𝐴 ·s ℎ ) ) -s ( 𝑔 ·s ℎ ) ) } ∪ { 𝑖 ∣ ∃ 𝑗 ∈ ( R ‘ 𝐴 ) ∃ 𝑘 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑗 ·s 𝐵 ) +s ( 𝐴 ·s 𝑘 ) ) -s ( 𝑗 ·s 𝑘 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑙 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐴 ) ∃ 𝑛 ∈ ( R ‘ 𝐵 ) 𝑙 = ( ( ( 𝑚 ·s 𝐵 ) +s ( 𝐴 ·s 𝑛 ) ) -s ( 𝑚 ·s 𝑛 ) ) } ∪ { 𝑜 ∣ ∃ 𝑥 ∈ ( R ‘ 𝐴 ) ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑜 = ( ( ( 𝑥 ·s 𝐵 ) +s ( 𝐴 ·s 𝑦 ) ) -s ( 𝑥 ·s 𝑦 ) ) } ) ) )
14	3 13	sylibr	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } ∧ { ( 𝐴 ·s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑐 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑑 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )