Theorem mulsproplem11

Description: Lemma for surreal multiplication. Under the inductive hypothesis, demonstrate closure of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
	mulsproplem9.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulsproplem9.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	mulsproplem11	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
2		mulsproplem9.1	⊢ ( 𝜑 → 𝐴 ∈ No )
3		mulsproplem9.2	⊢ ( 𝜑 → 𝐵 ∈ No )
4	1 2 3	mulsproplem10	⊢ ( 𝜑 → ( ( 𝐴 ·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 𝑤 ) ) } ) ) )
5	4	simp1d	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )