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

Theorem mulsasslem3 27981
Description: Lemma for mulsass 27982. Demonstrate the central equality. (Contributed by Scott Fenton, 10-Mar-2025.)
Hypotheses
Ref Expression
mulsasslem3.1 (๐œ‘ โ†’ ๐ด โˆˆ No )
mulsasslem3.2 (๐œ‘ โ†’ ๐ต โˆˆ No )
mulsasslem3.3 (๐œ‘ โ†’ ๐ถ โˆˆ No )
mulsasslem3.4 ๐‘ƒ โІ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))
mulsasslem3.5 ๐‘„ โІ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))
mulsasslem3.6 ๐‘… โІ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))
mulsasslem3.7 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
mulsasslem3.8 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
mulsasslem3.9 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐‘ง๐‘‚)))
mulsasslem3.10 (๐œ‘ โ†’ โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
mulsasslem3.11 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐ถ)))
mulsasslem3.12 (๐œ‘ โ†’ โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
mulsasslem3.13 (๐œ‘ โ†’ โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐ด ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐ต ยทs ๐‘ง๐‘‚)))
Assertion
Ref Expression
mulsasslem3 (๐œ‘ โ†’ (โˆƒ๐‘ฅ โˆˆ ๐‘ƒ โˆƒ๐‘ฆ โˆˆ ๐‘„ โˆƒ๐‘ง โˆˆ ๐‘… ๐‘Ž = ((((((๐‘ฅ ยท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 ๐‘ง))))))
Distinct variable groups:   ๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚,๐ด   ๐ต,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚   ๐ถ,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚   ๐‘ฅ,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚   ๐‘ฆ,๐‘ฆ๐‘‚,๐‘ง๐‘‚   ๐‘ง,๐‘ง๐‘‚,๐‘ฆ   ๐‘ฆ,๐‘ƒ,๐‘ง   ๐‘ง,๐‘„   ๐‘ฅ,๐‘ฆ,๐‘ง,๐œ‘
Allowed substitution hints:   ๐œ‘(๐‘Ž,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚)   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘Ž)   ๐ต(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘Ž)   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘Ž)   ๐‘ƒ(๐‘ฅ,๐‘Ž,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚)   ๐‘„(๐‘ฅ,๐‘ฆ,๐‘Ž,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚)   ๐‘…(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘Ž,๐‘ฅ๐‘‚,๐‘ฆ๐‘‚,๐‘ง๐‘‚)

Proof of Theorem mulsasslem3
StepHypRef Expression
1 oveq1 7408 . . . . . . . . . . 11 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (๐‘ฅ๐‘‚ ยทs ๐ต) = (๐‘ฅ ยทs ๐ต))
21oveq1d 7416 . . . . . . . . . 10 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ ((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐ถ) = ((๐‘ฅ ยทs ๐ต) ยทs ๐ถ))
3 oveq1 7408 . . . . . . . . . 10 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐ถ)) = (๐‘ฅ ยทs (๐ต ยทs ๐ถ)))
42, 3eqeq12d 2740 . . . . . . . . 9 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐ถ)) โ†” ((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) = (๐‘ฅ ยทs (๐ต ยทs ๐ถ))))
5 mulsasslem3.11 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐ถ)))
65adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐ถ)))
7 mulsasslem3.4 . . . . . . . . . 10 ๐‘ƒ โІ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))
8 simprll 776 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ฅ โˆˆ ๐‘ƒ)
97, 8sselid 3972 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ฅ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด)))
104, 6, 9rspcdva 3605 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) = (๐‘ฅ ยทs (๐ต ยทs ๐ถ)))
11 oveq2 7409 . . . . . . . . . . . . 13 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐ด ยทs ๐‘ฆ๐‘‚) = (๐ด ยทs ๐‘ฆ))
1211oveq1d 7416 . . . . . . . . . . . 12 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ ((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ))
13 oveq1 7408 . . . . . . . . . . . . 13 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐‘ฆ๐‘‚ ยทs ๐ถ) = (๐‘ฆ ยทs ๐ถ))
1413oveq2d 7417 . . . . . . . . . . . 12 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)) = (๐ด ยทs (๐‘ฆ ยทs ๐ถ)))
1512, 14eqeq12d 2740 . . . . . . . . . . 11 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)) โ†” ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ) = (๐ด ยทs (๐‘ฆ ยทs ๐ถ))))
16 mulsasslem3.12 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
1716adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
18 mulsasslem3.5 . . . . . . . . . . . 12 ๐‘„ โІ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))
19 simprlr 777 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ฆ โˆˆ ๐‘„)
2018, 19sselid 3972 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ฆ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต)))
2115, 17, 20rspcdva 3605 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ) = (๐ด ยทs (๐‘ฆ ยทs ๐ถ)))
22 oveq2 7409 . . . . . . . . . . . . . 14 (๐‘ง๐‘‚ = ๐‘ง โ†’ ((๐ด ยทs ๐ต) ยทs ๐‘ง๐‘‚) = ((๐ด ยทs ๐ต) ยทs ๐‘ง))
23 oveq2 7409 . . . . . . . . . . . . . . 15 (๐‘ง๐‘‚ = ๐‘ง โ†’ (๐ต ยทs ๐‘ง๐‘‚) = (๐ต ยทs ๐‘ง))
2423oveq2d 7417 . . . . . . . . . . . . . 14 (๐‘ง๐‘‚ = ๐‘ง โ†’ (๐ด ยทs (๐ต ยทs ๐‘ง๐‘‚)) = (๐ด ยทs (๐ต ยทs ๐‘ง)))
2522, 24eqeq12d 2740 . . . . . . . . . . . . 13 (๐‘ง๐‘‚ = ๐‘ง โ†’ (((๐ด ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐ต ยทs ๐‘ง๐‘‚)) โ†” ((๐ด ยทs ๐ต) ยทs ๐‘ง) = (๐ด ยทs (๐ต ยทs ๐‘ง))))
26 mulsasslem3.13 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐ด ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐ต ยทs ๐‘ง๐‘‚)))
2726adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐ด ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐ต ยทs ๐‘ง๐‘‚)))
28 mulsasslem3.6 . . . . . . . . . . . . . 14 ๐‘… โІ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))
29 simprr 770 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ง โˆˆ ๐‘…)
3028, 29sselid 3972 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ง โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ)))
3125, 27, 30rspcdva 3605 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ๐ต) ยทs ๐‘ง) = (๐ด ยทs (๐ต ยทs ๐‘ง)))
32 leftssno 27723 . . . . . . . . . . . . . . . . . . . . . 22 ( L โ€˜๐ด) โІ No
33 rightssno 27724 . . . . . . . . . . . . . . . . . . . . . 22 ( R โ€˜๐ด) โІ No
3432, 33unssi 4177 . . . . . . . . . . . . . . . . . . . . 21 (( L โ€˜๐ด) โˆช ( R โ€˜๐ด)) โІ No
357, 34sstri 3983 . . . . . . . . . . . . . . . . . . . 20 ๐‘ƒ โІ No
3635, 8sselid 3972 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ฅ โˆˆ No )
37 mulsasslem3.2 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐ต โˆˆ No )
3837adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐ต โˆˆ No )
3936, 38mulscld 27951 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs ๐ต) โˆˆ No )
40 leftssno 27723 . . . . . . . . . . . . . . . . . . . . 21 ( L โ€˜๐ถ) โІ No
41 rightssno 27724 . . . . . . . . . . . . . . . . . . . . 21 ( R โ€˜๐ถ) โІ No
4240, 41unssi 4177 . . . . . . . . . . . . . . . . . . . 20 (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ)) โІ No
4328, 42sstri 3983 . . . . . . . . . . . . . . . . . . 19 ๐‘… โІ No
4443, 29sselid 3972 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ง โˆˆ No )
4539, 44mulscld 27951 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) โˆˆ No )
46 mulsasslem3.1 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐ด โˆˆ No )
4746adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐ด โˆˆ No )
48 leftssno 27723 . . . . . . . . . . . . . . . . . . . . . 22 ( L โ€˜๐ต) โІ No
49 rightssno 27724 . . . . . . . . . . . . . . . . . . . . . 22 ( R โ€˜๐ต) โІ No
5048, 49unssi 4177 . . . . . . . . . . . . . . . . . . . . 21 (( L โ€˜๐ต) โˆช ( R โ€˜๐ต)) โІ No
5118, 50sstri 3983 . . . . . . . . . . . . . . . . . . . 20 ๐‘„ โІ No
5251, 19sselid 3972 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐‘ฆ โˆˆ No )
5347, 52mulscld 27951 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs ๐‘ฆ) โˆˆ No )
5453, 44mulscld 27951 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) โˆˆ No )
5545, 54addscomd 27800 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) = (((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง)))
5655oveq1d 7416 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) = ((((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)))
5736, 52mulscld 27951 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs ๐‘ฆ) โˆˆ No )
5857, 44mulscld 27951 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง) โˆˆ No )
5954, 45, 58addsubsassd 27905 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) = (((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง))))
6056, 59eqtrd 2764 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) = (((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง))))
6160oveq1d 7416 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = ((((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง))) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)))
6245, 58subscld 27889 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) โˆˆ No )
63 mulsasslem3.3 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ถ โˆˆ No )
6463adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ๐ถ โˆˆ No )
6557, 64mulscld 27951 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ) โˆˆ No )
6654, 62, 65addsassd 27839 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง))) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = (((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ))))
6711oveq1d 7416 . . . . . . . . . . . . . . . 16 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ ((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚))
68 oveq1 7408 . . . . . . . . . . . . . . . . 17 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚) = (๐‘ฆ ยทs ๐‘ง๐‘‚))
6968oveq2d 7417 . . . . . . . . . . . . . . . 16 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)) = (๐ด ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚)))
7067, 69eqeq12d 2740 . . . . . . . . . . . . . . 15 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)) โ†” ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚))))
71 oveq2 7409 . . . . . . . . . . . . . . . 16 (๐‘ง๐‘‚ = ๐‘ง โ†’ ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚) = ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง))
72 oveq2 7409 . . . . . . . . . . . . . . . . 17 (๐‘ง๐‘‚ = ๐‘ง โ†’ (๐‘ฆ ยทs ๐‘ง๐‘‚) = (๐‘ฆ ยทs ๐‘ง))
7372oveq2d 7417 . . . . . . . . . . . . . . . 16 (๐‘ง๐‘‚ = ๐‘ง โ†’ (๐ด ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚)) = (๐ด ยทs (๐‘ฆ ยทs ๐‘ง)))
7471, 73eqeq12d 2740 . . . . . . . . . . . . . . 15 (๐‘ง๐‘‚ = ๐‘ง โ†’ (((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚)) โ†” ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) = (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))))
75 mulsasslem3.10 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
7675adantr 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐ด ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐ด ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
7770, 74, 76, 20, 30rspc2dv 3618 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) = (๐ด ยทs (๐‘ฆ ยทs ๐‘ง)))
7845, 65, 58addsubsd 27906 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) = ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)))
791oveq1d 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ ((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง๐‘‚))
80 oveq1 7408 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐‘ง๐‘‚)) = (๐‘ฅ ยทs (๐ต ยทs ๐‘ง๐‘‚)))
8179, 80eqeq12d 2740 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐‘ง๐‘‚)) โ†” ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐‘ฅ ยทs (๐ต ยทs ๐‘ง๐‘‚))))
82 oveq2 7409 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง๐‘‚ = ๐‘ง โ†’ ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง))
8323oveq2d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง๐‘‚ = ๐‘ง โ†’ (๐‘ฅ ยทs (๐ต ยทs ๐‘ง๐‘‚)) = (๐‘ฅ ยทs (๐ต ยทs ๐‘ง)))
8482, 83eqeq12d 2740 . . . . . . . . . . . . . . . . . . 19 (๐‘ง๐‘‚ = ๐‘ง โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐‘ฅ ยทs (๐ต ยทs ๐‘ง๐‘‚)) โ†” ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) = (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))))
85 mulsasslem3.9 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐‘ง๐‘‚)))
8685adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐‘ฅ๐‘‚ ยทs ๐ต) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐ต ยทs ๐‘ง๐‘‚)))
8781, 84, 86, 9, 30rspc2dv 3618 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) = (๐‘ฅ ยทs (๐ต ยทs ๐‘ง)))
88 oveq1 7408 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) = (๐‘ฅ ยทs ๐‘ฆ๐‘‚))
8988oveq1d 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ ((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = ((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ))
90 oveq1 7408 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)) = (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
9189, 90eqeq12d 2740 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)) โ†” ((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ))))
92 oveq2 7409 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐‘ฅ ยทs ๐‘ฆ๐‘‚) = (๐‘ฅ ยทs ๐‘ฆ))
9392oveq1d 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ ((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ))
9413oveq2d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)))
9593, 94eqeq12d 2740 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)) โ†” ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ))))
96 mulsasslem3.8 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
9796adantr 480 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐ถ) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐ถ)))
9891, 95, 97, 9, 20rspc2dv 3618 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)))
9987, 98oveq12d 7419 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = ((๐‘ฅ ยทs (๐ต ยทs ๐‘ง)) +s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ))))
10038, 44mulscld 27951 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ต ยทs ๐‘ง) โˆˆ No )
10136, 100mulscld 27951 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs (๐ต ยทs ๐‘ง)) โˆˆ No )
10252, 64mulscld 27951 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฆ ยทs ๐ถ) โˆˆ No )
10336, 102mulscld 27951 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) โˆˆ No )
104101, 103addscomd 27800 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs (๐ต ยทs ๐‘ง)) +s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ))) = ((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))))
10599, 104eqtrd 2764 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = ((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))))
10688oveq1d 7416 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ ((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = ((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚))
107 oveq1 7408 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)) = (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
108106, 107eqeq12d 2740 . . . . . . . . . . . . . . . . 17 (๐‘ฅ๐‘‚ = ๐‘ฅ โ†’ (((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)) โ†” ((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚))))
10992oveq1d 7416 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ ((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚))
11068oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚)))
111109, 110eqeq12d 2740 . . . . . . . . . . . . . . . . 17 (๐‘ฆ๐‘‚ = ๐‘ฆ โ†’ (((๐‘ฅ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐‘ฅ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)) โ†” ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚))))
112 oveq2 7409 . . . . . . . . . . . . . . . . . 18 (๐‘ง๐‘‚ = ๐‘ง โ†’ ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚) = ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง))
11372oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (๐‘ง๐‘‚ = ๐‘ง โ†’ (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚)) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง)))
114112, 113eqeq12d 2740 . . . . . . . . . . . . . . . . 17 (๐‘ง๐‘‚ = ๐‘ง โ†’ (((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง๐‘‚) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง๐‘‚)) โ†” ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))))
115 mulsasslem3.7 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
116115adantr 480 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))โˆ€๐‘ฆ๐‘‚ โˆˆ (( L โ€˜๐ต) โˆช ( R โ€˜๐ต))โˆ€๐‘ง๐‘‚ โˆˆ (( L โ€˜๐ถ) โˆช ( R โ€˜๐ถ))((๐‘ฅ๐‘‚ ยทs ๐‘ฆ๐‘‚) ยทs ๐‘ง๐‘‚) = (๐‘ฅ๐‘‚ ยทs (๐‘ฆ๐‘‚ ยทs ๐‘ง๐‘‚)))
117108, 111, 114, 116, 9, 20, 30rspc3dv 3621 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง) = (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง)))
118105, 117oveq12d 7419 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) = (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))))
11978, 118eqtr3d 2766 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))))
12077, 119oveq12d 7419 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง) +s ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ))) = ((๐ด ยทs (๐‘ฆ ยทs ๐‘ง)) +s (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง)))))
12161, 66, 1203eqtrd 2768 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) +s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = ((๐ด ยทs (๐‘ฆ ยทs ๐‘ง)) +s (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง)))))
12231, 121oveq12d 7419 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยท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 ๐‘ง))))))
12347, 38mulscld 27951 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
124123, 44mulscld 27951 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ๐ต) ยทs ๐‘ง) โˆˆ No )
12545, 54addscld 27813 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) โˆˆ No )
126125, 58subscld 27889 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) โˆˆ No )
127124, 126, 65subsubs4d 27917 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐ถ))))
12847, 100mulscld 27951 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs (๐ต ยทs ๐‘ง)) โˆˆ No )
12952, 44mulscld 27951 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฆ ยทs ๐‘ง) โˆˆ No )
13047, 129mulscld 27951 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs (๐‘ฆ ยทs ๐‘ง)) โˆˆ No )
131103, 101addscld 27813 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) โˆˆ No )
13236, 129mulscld 27951 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง)) โˆˆ No )
133131, 132subscld 27889 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))) โˆˆ No )
134128, 130, 133subsubs4d 27917 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยท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 ๐‘ง))))))
135122, 127, 1343eqtr4d 2774 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐‘ง)))))
13621, 135oveq12d 7419 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยท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 ๐‘ง))))))
13753, 64mulscld 27951 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ) โˆˆ No )
138124, 126subscld 27889 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยทs ๐ต) ยทs ๐‘ง) -s ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง))) โˆˆ No )
139137, 138, 65addsubsd 27906 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐‘ง)))))
140137, 138, 65addsubsassd 27905 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐ถ))))
141139, 140eqtr3d 2766 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐ถ))))
14247, 102mulscld 27951 . . . . . . . . . . . 12 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs (๐‘ฆ ยทs ๐ถ)) โˆˆ No )
143142, 128, 130addsubsassd 27905 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))) = ((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s ((๐ด ยทs (๐ต ยทs ๐‘ง)) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง)))))
144143oveq1d 7416 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐‘ง)))))
145128, 130subscld 27889 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs (๐ต ยทs ๐‘ง)) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))) โˆˆ No )
146142, 145, 133addsubsassd 27905 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยท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 ๐‘ง))))))
147144, 146eqtrd 2764 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐‘ง))))))
148136, 141, 1473eqtr4d 2774 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐ด ยท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 ๐‘ง)))))
14910, 148oveq12d 7419 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยท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 ๐‘ง))))))
15039, 64mulscld 27951 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) โˆˆ No )
151150, 137addscld 27813 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)) โˆˆ No )
152151, 65subscld 27889 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) โˆˆ No )
153152, 124, 126addsubsassd 27905 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((((๐‘ฅ ยท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 ๐‘ง)))))
154150, 137, 65addsubsassd 27905 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = (((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s (((๐ด ยทs ๐‘ฆ) ยทs ๐ถ) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ))))
155154oveq1d 7416 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((((๐‘ฅ ยท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 ๐‘ง)))))
156137, 65subscld 27889 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยทs ๐‘ฆ) ยทs ๐ถ) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) โˆˆ No )
157150, 156, 138addsassd 27839 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยท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 ๐‘ง))))))
158153, 155, 1573eqtrd 2768 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((((๐‘ฅ ยท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 ๐‘ง))))))
15938, 64mulscld 27951 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ต ยทs ๐ถ) โˆˆ No )
16036, 159mulscld 27951 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs (๐ต ยทs ๐ถ)) โˆˆ No )
161142, 128addscld 27813 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))) โˆˆ No )
162161, 130subscld 27889 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))) โˆˆ No )
163160, 162, 133addsubsassd 27905 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยท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 ๐‘ง))))))
164149, 158, 1633eqtr4d 2774 . . . . . 6 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((((๐‘ฅ ยท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 ๐‘ง)))))
16539, 53addscld 27813 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) โˆˆ No )
166165, 57, 64subsdird 27975 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) -s (๐‘ฅ ยทs ๐‘ฆ)) ยทs ๐ถ) = ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) ยทs ๐ถ) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)))
16739, 53, 64addsdird 27973 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) ยทs ๐ถ) = (((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)))
168167oveq1d 7416 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) ยทs ๐ถ) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) = ((((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)))
169166, 168eqtrd 2764 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) -s (๐‘ฅ ยทs ๐‘ฆ)) ยทs ๐ถ) = ((((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)))
170169oveq1d 7416 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) -s (๐‘ฅ ยทs ๐‘ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐‘ง)) = (((((๐‘ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐ถ)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐ถ)) +s ((๐ด ยทs ๐ต) ยทs ๐‘ง)))
171165, 57, 44subsdird 27975 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) -s (๐‘ฅ ยทs ๐‘ฆ)) ยทs ๐‘ง) = ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)))
17239, 53, 44addsdird 27973 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) ยทs ๐‘ง) = (((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)))
173172oveq1d 7416 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) ยทs ๐‘ง) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)) = ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)))
174171, 173eqtrd 2764 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((๐‘ฅ ยทs ๐ต) +s (๐ด ยทs ๐‘ฆ)) -s (๐‘ฅ ยทs ๐‘ฆ)) ยทs ๐‘ง) = ((((๐‘ฅ ยทs ๐ต) ยทs ๐‘ง) +s ((๐ด ยทs ๐‘ฆ) ยทs ๐‘ง)) -s ((๐‘ฅ ยทs ๐‘ฆ) ยทs ๐‘ง)))
175170, 174oveq12d 7419 . . . . . 6 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((((๐‘ฅ ยท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 ๐‘ง))))
176102, 100addscld 27813 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง)) โˆˆ No )
17747, 176, 129subsdid 27974 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs (((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง)) -s (๐‘ฆ ยทs ๐‘ง))) = ((๐ด ยทs ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))))
17847, 102, 100addsdid 27972 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง))) = ((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))))
179178oveq1d 7416 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐ด ยทs ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))) = (((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))))
180177, 179eqtrd 2764 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐ด ยทs (((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง)) -s (๐‘ฆ ยทs ๐‘ง))) = (((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง))))
181180oveq2d 7417 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง)) -s (๐‘ฆ ยทs ๐‘ง)))) = ((๐‘ฅ ยทs (๐ต ยทs ๐ถ)) +s (((๐ด ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐‘ง))) -s (๐ด ยทs (๐‘ฆ ยทs ๐‘ง)))))
18236, 176, 129subsdid 27974 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs (((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง)) -s (๐‘ฆ ยทs ๐‘ง))) = ((๐‘ฅ ยทs ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))))
18336, 102, 100addsdid 27972 . . . . . . . . 9 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง))) = ((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))))
184183oveq1d 7416 . . . . . . . 8 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((๐‘ฅ ยทs ((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))) = (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))))
185182, 184eqtrd 2764 . . . . . . 7 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘ฅ ยทs (((๐‘ฆ ยทs ๐ถ) +s (๐ต ยทs ๐‘ง)) -s (๐‘ฆ ยทs ๐‘ง))) = (((๐‘ฅ ยทs (๐‘ฆ ยทs ๐ถ)) +s (๐‘ฅ ยทs (๐ต ยทs ๐‘ง))) -s (๐‘ฅ ยทs (๐‘ฆ ยทs ๐‘ง))))
186181, 185oveq12d 7419 . . . . . 6 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (((๐‘ฅ ยท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 ๐‘ง)))))
187164, 175, 1863eqtr4d 2774 . . . . 5 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ ((((((๐‘ฅ ยท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 ๐‘ง)))))
188187eqeq2d 2735 . . . 4 ((๐œ‘ โˆง ((๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„) โˆง ๐‘ง โˆˆ ๐‘…)) โ†’ (๐‘Ž = ((((((๐‘ฅ ยท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 ๐‘ง))))))
189188anassrs 467 . . 3 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„)) โˆง ๐‘ง โˆˆ ๐‘…) โ†’ (๐‘Ž = ((((((๐‘ฅ ยท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 ๐‘ง))))))
190189rexbidva 3168 . 2 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘„)) โ†’ (โˆƒ๐‘ง โˆˆ ๐‘… ๐‘Ž = ((((((๐‘ฅ ยท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 ๐‘ง))))))
1911902rexbidva 3209 1 (๐œ‘ โ†’ (โˆƒ๐‘ฅ โˆˆ ๐‘ƒ โˆƒ๐‘ฆ โˆˆ ๐‘„ โˆƒ๐‘ง โˆˆ ๐‘… ๐‘Ž = ((((((๐‘ฅ ยท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 ๐‘ง))))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3053  โˆƒwrex 3062   โˆช cun 3938   โІ wss 3940  โ€˜cfv 6533  (class class class)co 7401   No csur 27489   L cleft 27688   R cright 27689   +s cadds 27792   -s csubs 27849   ยทs cmuls 27922
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 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
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 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8661  df-no 27492  df-slt 27493  df-bday 27494  df-sle 27594  df-sslt 27630  df-scut 27632  df-0s 27673  df-made 27690  df-old 27691  df-left 27693  df-right 27694  df-norec 27771  df-norec2 27782  df-adds 27793  df-negs 27850  df-subs 27851  df-muls 27923
This theorem is referenced by:  mulsass  27982
  Copyright terms: Public domain W3C validator