MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsrid Structured version   Visualization version   GIF version

Theorem mulsrid 27963
Description: Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025.)
Assertion
Ref Expression
mulsrid (๐ด โˆˆ No โ†’ (๐ด ยทs 1s ) = ๐ด)

Proof of Theorem mulsrid
Dummy variables ๐‘ฅ ๐‘ฅ๐‘‚ ๐‘Ž ๐‘ ๐‘ ๐‘‘ ๐‘ ๐‘ž ๐‘Ÿ ๐‘  ๐‘ก ๐‘ข ๐‘ฃ ๐‘ค are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7411 . . 3 (๐‘ฅ = ๐‘ฅ๐‘‚ โ†’ (๐‘ฅ ยทs 1s ) = (๐‘ฅ๐‘‚ ยทs 1s ))
2 id 22 . . 3 (๐‘ฅ = ๐‘ฅ๐‘‚ โ†’ ๐‘ฅ = ๐‘ฅ๐‘‚)
31, 2eqeq12d 2742 . 2 (๐‘ฅ = ๐‘ฅ๐‘‚ โ†’ ((๐‘ฅ ยทs 1s ) = ๐‘ฅ โ†” (๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚))
4 oveq1 7411 . . 3 (๐‘ฅ = ๐ด โ†’ (๐‘ฅ ยทs 1s ) = (๐ด ยทs 1s ))
5 id 22 . . 3 (๐‘ฅ = ๐ด โ†’ ๐‘ฅ = ๐ด)
64, 5eqeq12d 2742 . 2 (๐‘ฅ = ๐ด โ†’ ((๐‘ฅ ยทs 1s ) = ๐‘ฅ โ†” (๐ด ยทs 1s ) = ๐ด))
7 1sno 27710 . . . . . 6 1s โˆˆ No
8 mulsval 27959 . . . . . 6 ((๐‘ฅ โˆˆ No โˆง 1s โˆˆ No ) โ†’ (๐‘ฅ ยทs 1s ) = (({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) |s ({๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} โˆช {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))})))
97, 8mpan2 688 . . . . 5 (๐‘ฅ โˆˆ No โ†’ (๐‘ฅ ยทs 1s ) = (({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) |s ({๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} โˆช {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))})))
109adantr 480 . . . 4 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ฅ ยทs 1s ) = (({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) |s ({๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} โˆช {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))})))
11 elun1 4171 . . . . . . . . . . . . . . . . . . 19 (๐‘ โˆˆ ( L โ€˜๐‘ฅ) โ†’ ๐‘ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ)))
12 oveq1 7411 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ๐‘‚ = ๐‘ โ†’ (๐‘ฅ๐‘‚ ยทs 1s ) = (๐‘ ยทs 1s ))
13 id 22 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ๐‘‚ = ๐‘ โ†’ ๐‘ฅ๐‘‚ = ๐‘)
1412, 13eqeq12d 2742 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ๐‘‚ = ๐‘ โ†’ ((๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚ โ†” (๐‘ ยทs 1s ) = ๐‘))
1514rspcva 3604 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ)) โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ ยทs 1s ) = ๐‘)
1611, 15sylan 579 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆˆ ( L โ€˜๐‘ฅ) โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ ยทs 1s ) = ๐‘)
1716ancoms 458 . . . . . . . . . . . . . . . . 17 ((โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚ โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘ ยทs 1s ) = ๐‘)
1817adantll 711 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘ ยทs 1s ) = ๐‘)
19 muls01 27962 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ No โ†’ (๐‘ฅ ยทs 0s ) = 0s )
2019adantr 480 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ฅ ยทs 0s ) = 0s )
2120adantr 480 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘ฅ ยทs 0s ) = 0s )
2218, 21oveq12d 7422 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ ((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) = (๐‘ +s 0s ))
23 leftssno 27757 . . . . . . . . . . . . . . . . . 18 ( L โ€˜๐‘ฅ) โІ No
2423sseli 3973 . . . . . . . . . . . . . . . . 17 (๐‘ โˆˆ ( L โ€˜๐‘ฅ) โ†’ ๐‘ โˆˆ No )
2524adantl 481 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ ๐‘ โˆˆ No )
2625addsridd 27832 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘ +s 0s ) = ๐‘)
2722, 26eqtrd 2766 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ ((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) = ๐‘)
28 muls01 27962 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ No โ†’ (๐‘ ยทs 0s ) = 0s )
2925, 28syl 17 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘ ยทs 0s ) = 0s )
3027, 29oveq12d 7422 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )) = (๐‘ -s 0s ))
31 subsid1 27926 . . . . . . . . . . . . . 14 (๐‘ โˆˆ No โ†’ (๐‘ -s 0s ) = ๐‘)
3225, 31syl 17 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘ -s 0s ) = ๐‘)
3330, 32eqtrd 2766 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )) = ๐‘)
3433eqeq2d 2737 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )) โ†” ๐‘Ž = ๐‘))
35 equcom 2013 . . . . . . . . . . 11 (๐‘Ž = ๐‘ โ†” ๐‘ = ๐‘Ž)
3634, 35bitrdi 287 . . . . . . . . . 10 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ โˆˆ ( L โ€˜๐‘ฅ)) โ†’ (๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )) โ†” ๐‘ = ๐‘Ž))
3736rexbidva 3170 . . . . . . . . 9 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )) โ†” โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)๐‘ = ๐‘Ž))
38 left1s 27771 . . . . . . . . . . . 12 ( L โ€˜ 1s ) = { 0s }
3938rexeqi 3318 . . . . . . . . . . 11 (โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” โˆƒ๐‘ž โˆˆ { 0s }๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)))
40 0sno 27709 . . . . . . . . . . . . 13 0s โˆˆ No
4140elexi 3488 . . . . . . . . . . . 12 0s โˆˆ V
42 oveq2 7412 . . . . . . . . . . . . . . 15 (๐‘ž = 0s โ†’ (๐‘ฅ ยทs ๐‘ž) = (๐‘ฅ ยทs 0s ))
4342oveq2d 7420 . . . . . . . . . . . . . 14 (๐‘ž = 0s โ†’ ((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) = ((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )))
44 oveq2 7412 . . . . . . . . . . . . . 14 (๐‘ž = 0s โ†’ (๐‘ ยทs ๐‘ž) = (๐‘ ยทs 0s ))
4543, 44oveq12d 7422 . . . . . . . . . . . . 13 (๐‘ž = 0s โ†’ (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )))
4645eqeq2d 2737 . . . . . . . . . . . 12 (๐‘ž = 0s โ†’ (๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” ๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s ))))
4741, 46rexsn 4681 . . . . . . . . . . 11 (โˆƒ๐‘ž โˆˆ { 0s }๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” ๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )))
4839, 47bitri 275 . . . . . . . . . 10 (โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” ๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )))
4948rexbii 3088 . . . . . . . . 9 (โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ ยทs 0s )))
50 risset 3224 . . . . . . . . 9 (๐‘Ž โˆˆ ( L โ€˜๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)๐‘ = ๐‘Ž)
5137, 49, 503bitr4g 314 . . . . . . . 8 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” ๐‘Ž โˆˆ ( L โ€˜๐‘ฅ)))
5251eqabcdv 2862 . . . . . . 7 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} = ( L โ€˜๐‘ฅ))
53 rex0 4352 . . . . . . . . . . . 12 ยฌ โˆƒ๐‘  โˆˆ โˆ… ๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))
54 right1s 27772 . . . . . . . . . . . . 13 ( R โ€˜ 1s ) = โˆ…
5554rexeqi 3318 . . . . . . . . . . . 12 (โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†” โˆƒ๐‘  โˆˆ โˆ… ๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )))
5653, 55mtbir 323 . . . . . . . . . . 11 ยฌ โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))
5756a1i 11 . . . . . . . . . 10 (๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ) โ†’ ยฌ โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )))
5857nrex 3068 . . . . . . . . 9 ยฌ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))
5958abf 4397 . . . . . . . 8 {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))} = โˆ…
6059a1i 11 . . . . . . 7 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))} = โˆ…)
6152, 60uneq12d 4159 . . . . . 6 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) = (( L โ€˜๐‘ฅ) โˆช โˆ…))
62 un0 4385 . . . . . 6 (( L โ€˜๐‘ฅ) โˆช โˆ…) = ( L โ€˜๐‘ฅ)
6361, 62eqtrdi 2782 . . . . 5 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) = ( L โ€˜๐‘ฅ))
64 rex0 4352 . . . . . . . . . . . 12 ยฌ โˆƒ๐‘ข โˆˆ โˆ… ๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))
6554rexeqi 3318 . . . . . . . . . . . 12 (โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข)) โ†” โˆƒ๐‘ข โˆˆ โˆ… ๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข)))
6664, 65mtbir 323 . . . . . . . . . . 11 ยฌ โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))
6766a1i 11 . . . . . . . . . 10 (๐‘ก โˆˆ ( L โ€˜๐‘ฅ) โ†’ ยฌ โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข)))
6867nrex 3068 . . . . . . . . 9 ยฌ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))
6968abf 4397 . . . . . . . 8 {๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} = โˆ…
7069a1i 11 . . . . . . 7 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ {๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} = โˆ…)
71 elun2 4172 . . . . . . . . . . . . . . . . . . 19 (๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ) โ†’ ๐‘ฃ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ)))
72 oveq1 7411 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ๐‘‚ = ๐‘ฃ โ†’ (๐‘ฅ๐‘‚ ยทs 1s ) = (๐‘ฃ ยทs 1s ))
73 id 22 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ๐‘‚ = ๐‘ฃ โ†’ ๐‘ฅ๐‘‚ = ๐‘ฃ)
7472, 73eqeq12d 2742 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ๐‘‚ = ๐‘ฃ โ†’ ((๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚ โ†” (๐‘ฃ ยทs 1s ) = ๐‘ฃ))
7574rspcva 3604 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฃ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ)) โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ฃ ยทs 1s ) = ๐‘ฃ)
7671, 75sylan 579 . . . . . . . . . . . . . . . . . 18 ((๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ) โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ฃ ยทs 1s ) = ๐‘ฃ)
7776ancoms 458 . . . . . . . . . . . . . . . . 17 ((โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚ โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘ฃ ยทs 1s ) = ๐‘ฃ)
7877adantll 711 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘ฃ ยทs 1s ) = ๐‘ฃ)
7920adantr 480 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘ฅ ยทs 0s ) = 0s )
8078, 79oveq12d 7422 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ ((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) = (๐‘ฃ +s 0s ))
81 rightssno 27758 . . . . . . . . . . . . . . . . . 18 ( R โ€˜๐‘ฅ) โІ No
8281sseli 3973 . . . . . . . . . . . . . . . . 17 (๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ) โ†’ ๐‘ฃ โˆˆ No )
8382adantl 481 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ ๐‘ฃ โˆˆ No )
8483addsridd 27832 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘ฃ +s 0s ) = ๐‘ฃ)
8580, 84eqtrd 2766 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ ((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) = ๐‘ฃ)
86 muls01 27962 . . . . . . . . . . . . . . 15 (๐‘ฃ โˆˆ No โ†’ (๐‘ฃ ยทs 0s ) = 0s )
8783, 86syl 17 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘ฃ ยทs 0s ) = 0s )
8885, 87oveq12d 7422 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s )) = (๐‘ฃ -s 0s ))
89 subsid1 27926 . . . . . . . . . . . . . 14 (๐‘ฃ โˆˆ No โ†’ (๐‘ฃ -s 0s ) = ๐‘ฃ)
9083, 89syl 17 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘ฃ -s 0s ) = ๐‘ฃ)
9188, 90eqtrd 2766 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s )) = ๐‘ฃ)
9291eqeq2d 2737 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s )) โ†” ๐‘‘ = ๐‘ฃ))
9338rexeqi 3318 . . . . . . . . . . . 12 (โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” โˆƒ๐‘ค โˆˆ { 0s }๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)))
94 oveq2 7412 . . . . . . . . . . . . . . . 16 (๐‘ค = 0s โ†’ (๐‘ฅ ยทs ๐‘ค) = (๐‘ฅ ยทs 0s ))
9594oveq2d 7420 . . . . . . . . . . . . . . 15 (๐‘ค = 0s โ†’ ((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) = ((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )))
96 oveq2 7412 . . . . . . . . . . . . . . 15 (๐‘ค = 0s โ†’ (๐‘ฃ ยทs ๐‘ค) = (๐‘ฃ ยทs 0s ))
9795, 96oveq12d 7422 . . . . . . . . . . . . . 14 (๐‘ค = 0s โ†’ (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s )))
9897eqeq2d 2737 . . . . . . . . . . . . 13 (๐‘ค = 0s โ†’ (๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” ๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s ))))
9941, 98rexsn 4681 . . . . . . . . . . . 12 (โˆƒ๐‘ค โˆˆ { 0s }๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” ๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s )))
10093, 99bitri 275 . . . . . . . . . . 11 (โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” ๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs 0s )) -s (๐‘ฃ ยทs 0s )))
101 equcom 2013 . . . . . . . . . . 11 (๐‘ฃ = ๐‘‘ โ†” ๐‘‘ = ๐‘ฃ)
10292, 100, 1013bitr4g 314 . . . . . . . . . 10 (((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โˆง ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)) โ†’ (โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” ๐‘ฃ = ๐‘‘))
103102rexbidva 3170 . . . . . . . . 9 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)๐‘ฃ = ๐‘‘))
104 risset 3224 . . . . . . . . 9 (๐‘‘ โˆˆ ( R โ€˜๐‘ฅ) โ†” โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)๐‘ฃ = ๐‘‘)
105103, 104bitr4di 289 . . . . . . . 8 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค)) โ†” ๐‘‘ โˆˆ ( R โ€˜๐‘ฅ)))
106105eqabcdv 2862 . . . . . . 7 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))} = ( R โ€˜๐‘ฅ))
10770, 106uneq12d 4159 . . . . . 6 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ ({๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} โˆช {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))}) = (โˆ… โˆช ( R โ€˜๐‘ฅ)))
108 0un 4387 . . . . . 6 (โˆ… โˆช ( R โ€˜๐‘ฅ)) = ( R โ€˜๐‘ฅ)
109107, 108eqtrdi 2782 . . . . 5 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ ({๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} โˆช {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))}) = ( R โ€˜๐‘ฅ))
11063, 109oveq12d 7422 . . . 4 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ž โˆˆ ( L โ€˜ 1s )๐‘Ž = (((๐‘ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘  โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘Ÿ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) |s ({๐‘ โˆฃ โˆƒ๐‘ก โˆˆ ( L โ€˜๐‘ฅ)โˆƒ๐‘ข โˆˆ ( R โ€˜ 1s )๐‘ = (((๐‘ก ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ข)) -s (๐‘ก ยทs ๐‘ข))} โˆช {๐‘‘ โˆฃ โˆƒ๐‘ฃ โˆˆ ( R โ€˜๐‘ฅ)โˆƒ๐‘ค โˆˆ ( L โ€˜ 1s )๐‘‘ = (((๐‘ฃ ยทs 1s ) +s (๐‘ฅ ยทs ๐‘ค)) -s (๐‘ฃ ยทs ๐‘ค))})) = (( L โ€˜๐‘ฅ) |s ( R โ€˜๐‘ฅ)))
111 lrcut 27779 . . . . 5 (๐‘ฅ โˆˆ No โ†’ (( L โ€˜๐‘ฅ) |s ( R โ€˜๐‘ฅ)) = ๐‘ฅ)
112111adantr 480 . . . 4 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (( L โ€˜๐‘ฅ) |s ( R โ€˜๐‘ฅ)) = ๐‘ฅ)
11310, 110, 1123eqtrd 2770 . . 3 ((๐‘ฅ โˆˆ No โˆง โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚) โ†’ (๐‘ฅ ยทs 1s ) = ๐‘ฅ)
114113ex 412 . 2 (๐‘ฅ โˆˆ No โ†’ (โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐‘ฅ) โˆช ( R โ€˜๐‘ฅ))(๐‘ฅ๐‘‚ ยทs 1s ) = ๐‘ฅ๐‘‚ โ†’ (๐‘ฅ ยทs 1s ) = ๐‘ฅ))
1153, 6, 114noinds 27812 1 (๐ด โˆˆ No โ†’ (๐ด ยทs 1s ) = ๐ด)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098  {cab 2703  โˆ€wral 3055  โˆƒwrex 3064   โˆช cun 3941  โˆ…c0 4317  {csn 4623  โ€˜cfv 6536  (class class class)co 7404   No csur 27523   |s cscut 27665   0s c0s 27705   1s c1s 27706   L cleft 27722   R cright 27723   +s cadds 27826   -s csubs 27883   ยทs cmuls 27956
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-1o 8464  df-2o 8465  df-no 27526  df-slt 27527  df-bday 27528  df-sle 27628  df-sslt 27664  df-scut 27666  df-0s 27707  df-1s 27708  df-made 27724  df-old 27725  df-left 27727  df-right 27728  df-norec 27805  df-norec2 27816  df-adds 27827  df-negs 27884  df-subs 27885  df-muls 27957
This theorem is referenced by:  mulsridd  27964  mulslid  27992  remulscllem1  28178
  Copyright terms: Public domain W3C validator