mulsunif2

Description: Alternate expression for surreal multiplication. Note from Conway p. 19. (Contributed by Scott Fenton, 16-Mar-2025)

	Ref	Expression
Hypotheses	mulsunif2.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
	mulsunif2.2	⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
	mulsunif2.3	⊢ ( 𝜑 → 𝐴 = ( 𝐿 \|s 𝑅 ) )
	mulsunif2.4	⊢ ( 𝜑 → 𝐵 = ( 𝑀 \|s 𝑆 ) )
Assertion	mulsunif2	⊢ ( 𝜑 → ( 𝐴 ·_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		mulsunif2.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2		mulsunif2.2	⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3		mulsunif2.3	⊢ ( 𝜑 → 𝐴 = ( 𝐿 \|s 𝑅 ) )
4		mulsunif2.4	⊢ ( 𝜑 → 𝐵 = ( 𝑀 \|s 𝑆 ) )
5	1 2 3 4	mulsunif2lem	⊢ ( 𝜑 → ( 𝐴 ·_s 𝐵 ) = ( ( { 𝑒 ∣ ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑒 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) } ∪ { 𝑓 ∣ ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑓 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) } ) \|s ( { 𝑔 ∣ ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑔 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) } ∪ { ℎ ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 ℎ = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) } ) ) )
6		eqeq1	⊢ ( 𝑒 = 𝑎 → ( 𝑒 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ↔ 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ) )
7	6	2rexbidv	⊢ ( 𝑒 = 𝑎 → ( ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑒 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ↔ ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ) )
8		oveq2	⊢ ( 𝑖 = 𝑝 → ( 𝐴 -_s 𝑖 ) = ( 𝐴 -_s 𝑝 ) )
9	8	oveq1d	⊢ ( 𝑖 = 𝑝 → ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) = ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑗 ) ) )
10	9	oveq2d	⊢ ( 𝑖 = 𝑝 → ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) )
11	10	eqeq2d	⊢ ( 𝑖 = 𝑝 → ( 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ↔ 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ) )
12		oveq2	⊢ ( 𝑗 = 𝑞 → ( 𝐵 -_s 𝑗 ) = ( 𝐵 -_s 𝑞 ) )
13	12	oveq2d	⊢ ( 𝑗 = 𝑞 → ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑗 ) ) = ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) )
14	13	oveq2d	⊢ ( 𝑗 = 𝑞 → ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) )
15	14	eqeq2d	⊢ ( 𝑗 = 𝑞 → ( 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ↔ 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) ) )
16	11 15	cbvrex2vw	⊢ ( ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ↔ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) )
17	7 16	bitrdi	⊢ ( 𝑒 = 𝑎 → ( ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑒 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) ↔ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) ) )
18	17	cbvabv	⊢ { 𝑒 ∣ ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑒 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) } = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) }
19		eqeq1	⊢ ( 𝑓 = 𝑏 → ( 𝑓 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ↔ 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ) )
20	19	2rexbidv	⊢ ( 𝑓 = 𝑏 → ( ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑓 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ↔ ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ) )
21		oveq1	⊢ ( 𝑘 = 𝑟 → ( 𝑘 -_s 𝐴 ) = ( 𝑟 -_s 𝐴 ) )
22	21	oveq1d	⊢ ( 𝑘 = 𝑟 → ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) = ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) )
23	22	oveq2d	⊢ ( 𝑘 = 𝑟 → ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) )
24	23	eqeq2d	⊢ ( 𝑘 = 𝑟 → ( 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ↔ 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ) )
25		oveq1	⊢ ( 𝑙 = 𝑠 → ( 𝑙 -_s 𝐵 ) = ( 𝑠 -_s 𝐵 ) )
26	25	oveq2d	⊢ ( 𝑙 = 𝑠 → ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) = ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) )
27	26	oveq2d	⊢ ( 𝑙 = 𝑠 → ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) )
28	27	eqeq2d	⊢ ( 𝑙 = 𝑠 → ( 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ↔ 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) ) )
29	24 28	cbvrex2vw	⊢ ( ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) )
30	20 29	bitrdi	⊢ ( 𝑓 = 𝑏 → ( ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑓 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) ) )
31	30	cbvabv	⊢ { 𝑓 ∣ ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑓 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) } = { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) }
32	18 31	uneq12i	⊢ ( { 𝑒 ∣ ∃ 𝑖 ∈ 𝐿 ∃ 𝑗 ∈ 𝑀 𝑒 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑖 ) ·_s ( 𝐵 -_s 𝑗 ) ) ) } ∪ { 𝑓 ∣ ∃ 𝑘 ∈ 𝑅 ∃ 𝑙 ∈ 𝑆 𝑓 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑘 -_s 𝐴 ) ·_s ( 𝑙 -_s 𝐵 ) ) ) } ) = ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) } )
33		eqeq1	⊢ ( 𝑔 = 𝑐 → ( 𝑔 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ↔ 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ) )
34	33	2rexbidv	⊢ ( 𝑔 = 𝑐 → ( ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑔 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ↔ ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ) )
35		oveq2	⊢ ( 𝑚 = 𝑡 → ( 𝐴 -_s 𝑚 ) = ( 𝐴 -_s 𝑡 ) )
36	35	oveq1d	⊢ ( 𝑚 = 𝑡 → ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) = ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑛 -_s 𝐵 ) ) )
37	36	oveq2d	⊢ ( 𝑚 = 𝑡 → ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) )
38	37	eqeq2d	⊢ ( 𝑚 = 𝑡 → ( 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ↔ 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ) )
39		oveq1	⊢ ( 𝑛 = 𝑢 → ( 𝑛 -_s 𝐵 ) = ( 𝑢 -_s 𝐵 ) )
40	39	oveq2d	⊢ ( 𝑛 = 𝑢 → ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑛 -_s 𝐵 ) ) = ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) )
41	40	oveq2d	⊢ ( 𝑛 = 𝑢 → ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) )
42	41	eqeq2d	⊢ ( 𝑛 = 𝑢 → ( 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ↔ 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) ) )
43	38 42	cbvrex2vw	⊢ ( ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ↔ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) )
44	34 43	bitrdi	⊢ ( 𝑔 = 𝑐 → ( ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑔 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) ↔ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) ) )
45	44	cbvabv	⊢ { 𝑔 ∣ ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑔 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) } = { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) }
46		eqeq1	⊢ ( ℎ = 𝑑 → ( ℎ = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ↔ 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ) )
47	46	2rexbidv	⊢ ( ℎ = 𝑑 → ( ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 ℎ = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ↔ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ) )
48		oveq1	⊢ ( 𝑜 = 𝑣 → ( 𝑜 -_s 𝐴 ) = ( 𝑣 -_s 𝐴 ) )
49	48	oveq1d	⊢ ( 𝑜 = 𝑣 → ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) = ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) )
50	49	oveq2d	⊢ ( 𝑜 = 𝑣 → ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) )
51	50	eqeq2d	⊢ ( 𝑜 = 𝑣 → ( 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ↔ 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ) )
52		oveq2	⊢ ( 𝑥 = 𝑤 → ( 𝐵 -_s 𝑥 ) = ( 𝐵 -_s 𝑤 ) )
53	52	oveq2d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) = ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) )
54	53	oveq2d	⊢ ( 𝑥 = 𝑤 → ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) )
55	54	eqeq2d	⊢ ( 𝑥 = 𝑤 → ( 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ↔ 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) ) )
56	51 55	cbvrex2vw	⊢ ( ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ↔ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) )
57	47 56	bitrdi	⊢ ( ℎ = 𝑑 → ( ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 ℎ = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) ↔ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) ) )
58	57	cbvabv	⊢ { ℎ ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 ℎ = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) } = { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) }
59	45 58	uneq12i	⊢ ( { 𝑔 ∣ ∃ 𝑚 ∈ 𝐿 ∃ 𝑛 ∈ 𝑆 𝑔 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑚 ) ·_s ( 𝑛 -_s 𝐵 ) ) ) } ∪ { ℎ ∣ ∃ 𝑜 ∈ 𝑅 ∃ 𝑥 ∈ 𝑀 ℎ = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑜 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑥 ) ) ) } ) = ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) } )
60	32 59	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 𝑤 ) ) ) } ) )
61	5 60	eqtrdi	⊢ ( 𝜑 → ( 𝐴 ·_s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝐴 -_s 𝑝 ) ·_s ( 𝐵 -_s 𝑞 ) ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( 𝐴 ·_s 𝐵 ) -_s ( ( 𝑟 -_s 𝐴 ) ·_s ( 𝑠 -_s 𝐵 ) ) ) } ) \|s ( { 𝑐 ∣ ∃ 𝑡 ∈ 𝐿 ∃ 𝑢 ∈ 𝑆 𝑐 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝐴 -_s 𝑡 ) ·_s ( 𝑢 -_s 𝐵 ) ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ 𝑅 ∃ 𝑤 ∈ 𝑀 𝑑 = ( ( 𝐴 ·_s 𝐵 ) +_s ( ( 𝑣 -_s 𝐴 ) ·_s ( 𝐵 -_s 𝑤 ) ) ) } ) ) )

Metamath Proof Explorer

Theorem mulsunif2

Proof