Metamath Proof Explorer


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 ๐‘ค ) ) } ) ) )