ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulcmpblnrlemg GIF version

Theorem mulcmpblnrlemg 7752
Description: Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
Assertion
Ref Expression
mulcmpblnrlemg ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†))))))

Proof of Theorem mulcmpblnrlemg
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpllr 534 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐ต โˆˆ P)
2 simprlr 538 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐บ โˆˆ P)
3 mulclpr 7584 . . . . . . . . 9 ((๐ต โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ต ยทP ๐บ) โˆˆ P)
41, 2, 3syl2anc 411 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ต ยทP ๐บ) โˆˆ P)
5 simplrr 536 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐ท โˆˆ P)
6 simprrl 539 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐‘… โˆˆ P)
7 mulclpr 7584 . . . . . . . . 9 ((๐ท โˆˆ P โˆง ๐‘… โˆˆ P) โ†’ (๐ท ยทP ๐‘…) โˆˆ P)
85, 6, 7syl2anc 411 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP ๐‘…) โˆˆ P)
9 addclpr 7549 . . . . . . . 8 (((๐ต ยทP ๐บ) โˆˆ P โˆง (๐ท ยทP ๐‘…) โˆˆ P) โ†’ ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) โˆˆ P)
104, 8, 9syl2anc 411 . . . . . . 7 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) โˆˆ P)
11 simplrl 535 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐ถ โˆˆ P)
12 mulclpr 7584 . . . . . . . 8 ((๐ถ โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ถ ยทP ๐บ) โˆˆ P)
1311, 2, 12syl2anc 411 . . . . . . 7 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP ๐บ) โˆˆ P)
14 simprll 537 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐น โˆˆ P)
15 mulclpr 7584 . . . . . . . . 9 ((๐ต โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ต ยทP ๐น) โˆˆ P)
161, 14, 15syl2anc 411 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ต ยทP ๐น) โˆˆ P)
17 mulclpr 7584 . . . . . . . . 9 ((๐ถ โˆˆ P โˆง ๐‘… โˆˆ P) โ†’ (๐ถ ยทP ๐‘…) โˆˆ P)
1811, 6, 17syl2anc 411 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP ๐‘…) โˆˆ P)
19 addclpr 7549 . . . . . . . 8 (((๐ต ยทP ๐น) โˆˆ P โˆง (๐ถ ยทP ๐‘…) โˆˆ P) โ†’ ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)) โˆˆ P)
2016, 18, 19syl2anc 411 . . . . . . 7 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)) โˆˆ P)
21 addassprg 7591 . . . . . . 7 ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) โˆˆ P โˆง (๐ถ ยทP ๐บ) โˆˆ P โˆง ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)) โˆˆ P) โ†’ ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
2210, 13, 20, 21syl3anc 1248 . . . . . 6 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
2322adantr 276 . . . . 5 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
24 oveq2 5896 . . . . . . . . . . 11 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = (๐ท ยทP (๐บ +P ๐‘…)))
2524ad2antll 491 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = (๐ท ยทP (๐บ +P ๐‘…)))
26 simprrr 540 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐‘† โˆˆ P)
27 distrprg 7600 . . . . . . . . . . . 12 ((๐ท โˆˆ P โˆง ๐น โˆˆ P โˆง ๐‘† โˆˆ P) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†)))
285, 14, 26, 27syl3anc 1248 . . . . . . . . . . 11 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†)))
2928adantr 276 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†)))
30 distrprg 7600 . . . . . . . . . . . 12 ((๐ท โˆˆ P โˆง ๐บ โˆˆ P โˆง ๐‘… โˆˆ P) โ†’ (๐ท ยทP (๐บ +P ๐‘…)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
315, 2, 6, 30syl3anc 1248 . . . . . . . . . . 11 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP (๐บ +P ๐‘…)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
3231adantr 276 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (๐ท ยทP (๐บ +P ๐‘…)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
3325, 29, 323eqtr3d 2228 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
3433oveq2d 5904 . . . . . . . 8 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
35 simplll 533 . . . . . . . . . . 11 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ๐ด โˆˆ P)
36 mulclpr 7584 . . . . . . . . . . 11 ((๐ด โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ด ยทP ๐บ) โˆˆ P)
3735, 2, 36syl2anc 411 . . . . . . . . . 10 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ด ยทP ๐บ) โˆˆ P)
38 mulclpr 7584 . . . . . . . . . . 11 ((๐ท โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ท ยทP ๐บ) โˆˆ P)
395, 2, 38syl2anc 411 . . . . . . . . . 10 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP ๐บ) โˆˆ P)
40 addassprg 7591 . . . . . . . . . 10 (((๐ด ยทP ๐บ) โˆˆ P โˆง (๐ท ยทP ๐บ) โˆˆ P โˆง (๐ท ยทP ๐‘…) โˆˆ P) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
4137, 39, 8, 40syl3anc 1248 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
4241adantr 276 . . . . . . . 8 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
43 oveq1 5895 . . . . . . . . . . 11 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ต +P ๐ถ) ยทP ๐บ))
4443ad2antrl 490 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ต +P ๐ถ) ยทP ๐บ))
45 distrprg 7600 . . . . . . . . . . . . 13 ((๐บ โˆˆ P โˆง ๐ด โˆˆ P โˆง ๐ท โˆˆ P) โ†’ (๐บ ยทP (๐ด +P ๐ท)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท)))
462, 35, 5, 45syl3anc 1248 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐บ ยทP (๐ด +P ๐ท)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท)))
47 addclpr 7549 . . . . . . . . . . . . . 14 ((๐ด โˆˆ P โˆง ๐ท โˆˆ P) โ†’ (๐ด +P ๐ท) โˆˆ P)
4835, 5, 47syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ด +P ๐ท) โˆˆ P)
49 mulcomprg 7592 . . . . . . . . . . . . 13 (((๐ด +P ๐ท) โˆˆ P โˆง ๐บ โˆˆ P) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = (๐บ ยทP (๐ด +P ๐ท)))
5048, 2, 49syl2anc 411 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = (๐บ ยทP (๐ด +P ๐ท)))
51 mulcomprg 7592 . . . . . . . . . . . . . 14 ((๐ด โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ด ยทP ๐บ) = (๐บ ยทP ๐ด))
5235, 2, 51syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ด ยทP ๐บ) = (๐บ ยทP ๐ด))
53 mulcomprg 7592 . . . . . . . . . . . . . 14 ((๐ท โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ท ยทP ๐บ) = (๐บ ยทP ๐ท))
545, 2, 53syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP ๐บ) = (๐บ ยทP ๐ท))
5552, 54oveq12d 5906 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท)))
5646, 50, 553eqtr4d 2230 . . . . . . . . . . 11 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)))
5756adantr 276 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)))
58 distrprg 7600 . . . . . . . . . . . . 13 ((๐บ โˆˆ P โˆง ๐ต โˆˆ P โˆง ๐ถ โˆˆ P) โ†’ (๐บ ยทP (๐ต +P ๐ถ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ)))
592, 1, 11, 58syl3anc 1248 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐บ ยทP (๐ต +P ๐ถ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ)))
60 addclpr 7549 . . . . . . . . . . . . . 14 ((๐ต โˆˆ P โˆง ๐ถ โˆˆ P) โ†’ (๐ต +P ๐ถ) โˆˆ P)
611, 11, 60syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ต +P ๐ถ) โˆˆ P)
62 mulcomprg 7592 . . . . . . . . . . . . 13 (((๐ต +P ๐ถ) โˆˆ P โˆง ๐บ โˆˆ P) โ†’ ((๐ต +P ๐ถ) ยทP ๐บ) = (๐บ ยทP (๐ต +P ๐ถ)))
6361, 2, 62syl2anc 411 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต +P ๐ถ) ยทP ๐บ) = (๐บ ยทP (๐ต +P ๐ถ)))
64 mulcomprg 7592 . . . . . . . . . . . . . 14 ((๐ต โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ต ยทP ๐บ) = (๐บ ยทP ๐ต))
651, 2, 64syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ต ยทP ๐บ) = (๐บ ยทP ๐ต))
66 mulcomprg 7592 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ P โˆง ๐บ โˆˆ P) โ†’ (๐ถ ยทP ๐บ) = (๐บ ยทP ๐ถ))
6711, 2, 66syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP ๐บ) = (๐บ ยทP ๐ถ))
6865, 67oveq12d 5906 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ)))
6959, 63, 683eqtr4d 2230 . . . . . . . . . . 11 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต +P ๐ถ) ยทP ๐บ) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)))
7069adantr 276 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ต +P ๐ถ) ยทP ๐บ) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)))
7144, 57, 703eqtr3d 2228 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)))
7271oveq1d 5903 . . . . . . . 8 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
7334, 42, 723eqtr2d 2226 . . . . . . 7 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
74 mulclpr 7584 . . . . . . . . . 10 ((๐ท โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ท ยทP ๐น) โˆˆ P)
755, 14, 74syl2anc 411 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP ๐น) โˆˆ P)
76 mulclpr 7584 . . . . . . . . . 10 ((๐ท โˆˆ P โˆง ๐‘† โˆˆ P) โ†’ (๐ท ยทP ๐‘†) โˆˆ P)
775, 26, 76syl2anc 411 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP ๐‘†) โˆˆ P)
78 addcomprg 7590 . . . . . . . . . 10 ((๐‘ฅ โˆˆ P โˆง ๐‘ฆ โˆˆ P) โ†’ (๐‘ฅ +P ๐‘ฆ) = (๐‘ฆ +P ๐‘ฅ))
7978adantl 277 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐‘ฅ โˆˆ P โˆง ๐‘ฆ โˆˆ P)) โ†’ (๐‘ฅ +P ๐‘ฆ) = (๐‘ฆ +P ๐‘ฅ))
80 addassprg 7591 . . . . . . . . . 10 ((๐‘ฅ โˆˆ P โˆง ๐‘ฆ โˆˆ P โˆง ๐‘ง โˆˆ P) โ†’ ((๐‘ฅ +P ๐‘ฆ) +P ๐‘ง) = (๐‘ฅ +P (๐‘ฆ +P ๐‘ง)))
8180adantl 277 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐‘ฅ โˆˆ P โˆง ๐‘ฆ โˆˆ P โˆง ๐‘ง โˆˆ P)) โ†’ ((๐‘ฅ +P ๐‘ฆ) +P ๐‘ง) = (๐‘ฅ +P (๐‘ฆ +P ๐‘ง)))
8237, 75, 77, 79, 81caov12d 6069 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))))
8382adantr 276 . . . . . . 7 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))))
844, 13, 8, 79, 81caov32d 6068 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)))
8584adantr 276 . . . . . . 7 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)))
8673, 83, 853eqtr3d 2228 . . . . . 6 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)))
8786oveq1d 5903 . . . . 5 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
88 oveq1 5895 . . . . . . . . . . . 12 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = ((๐ต +P ๐ถ) ยทP ๐น))
8988adantl 277 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐ด +P ๐ท) = (๐ต +P ๐ถ)) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = ((๐ต +P ๐ถ) ยทP ๐น))
90 distrprg 7600 . . . . . . . . . . . . . 14 ((๐น โˆˆ P โˆง ๐ด โˆˆ P โˆง ๐ท โˆˆ P) โ†’ (๐น ยทP (๐ด +P ๐ท)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท)))
9114, 35, 5, 90syl3anc 1248 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐น ยทP (๐ด +P ๐ท)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท)))
92 mulcomprg 7592 . . . . . . . . . . . . . 14 (((๐ด +P ๐ท) โˆˆ P โˆง ๐น โˆˆ P) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = (๐น ยทP (๐ด +P ๐ท)))
9348, 14, 92syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = (๐น ยทP (๐ด +P ๐ท)))
94 mulcomprg 7592 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ด ยทP ๐น) = (๐น ยทP ๐ด))
9535, 14, 94syl2anc 411 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ด ยทP ๐น) = (๐น ยทP ๐ด))
96 mulcomprg 7592 . . . . . . . . . . . . . . 15 ((๐ท โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ท ยทP ๐น) = (๐น ยทP ๐ท))
975, 14, 96syl2anc 411 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ท ยทP ๐น) = (๐น ยทP ๐ท))
9895, 97oveq12d 5906 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท)))
9991, 93, 983eqtr4d 2230 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)))
10099adantr 276 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐ด +P ๐ท) = (๐ต +P ๐ถ)) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)))
101 distrprg 7600 . . . . . . . . . . . . . 14 ((๐น โˆˆ P โˆง ๐ต โˆˆ P โˆง ๐ถ โˆˆ P) โ†’ (๐น ยทP (๐ต +P ๐ถ)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ)))
10214, 1, 11, 101syl3anc 1248 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐น ยทP (๐ต +P ๐ถ)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ)))
103 mulcomprg 7592 . . . . . . . . . . . . . 14 (((๐ต +P ๐ถ) โˆˆ P โˆง ๐น โˆˆ P) โ†’ ((๐ต +P ๐ถ) ยทP ๐น) = (๐น ยทP (๐ต +P ๐ถ)))
10461, 14, 103syl2anc 411 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต +P ๐ถ) ยทP ๐น) = (๐น ยทP (๐ต +P ๐ถ)))
105 mulcomprg 7592 . . . . . . . . . . . . . . 15 ((๐ต โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ต ยทP ๐น) = (๐น ยทP ๐ต))
1061, 14, 105syl2anc 411 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ต ยทP ๐น) = (๐น ยทP ๐ต))
107 mulcomprg 7592 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ถ ยทP ๐น) = (๐น ยทP ๐ถ))
10811, 14, 107syl2anc 411 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP ๐น) = (๐น ยทP ๐ถ))
109106, 108oveq12d 5906 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ)))
110102, 104, 1093eqtr4d 2230 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต +P ๐ถ) ยทP ๐น) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)))
111110adantr 276 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐ด +P ๐ท) = (๐ต +P ๐ถ)) โ†’ ((๐ต +P ๐ถ) ยทP ๐น) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)))
11289, 100, 1113eqtr3d 2228 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐ด +P ๐ท) = (๐ต +P ๐ถ)) โ†’ ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)))
113112oveq1d 5903 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐ด +P ๐ท) = (๐ต +P ๐ถ)) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)))
114113adantrr 479 . . . . . . . 8 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)))
115 mulclpr 7584 . . . . . . . . . . . . 13 ((๐ถ โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ถ ยทP ๐น) โˆˆ P)
11611, 14, 115syl2anc 411 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP ๐น) โˆˆ P)
117 mulclpr 7584 . . . . . . . . . . . . 13 ((๐ถ โˆˆ P โˆง ๐‘† โˆˆ P) โ†’ (๐ถ ยทP ๐‘†) โˆˆ P)
11811, 26, 117syl2anc 411 . . . . . . . . . . . 12 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP ๐‘†) โˆˆ P)
119 addassprg 7591 . . . . . . . . . . . 12 (((๐ต ยทP ๐น) โˆˆ P โˆง (๐ถ ยทP ๐น) โˆˆ P โˆง (๐ถ ยทP ๐‘†) โˆˆ P) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))))
12016, 116, 118, 119syl3anc 1248 . . . . . . . . . . 11 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))))
121120adantr 276 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))))
122 oveq2 5896 . . . . . . . . . . . . 13 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = (๐ถ ยทP (๐บ +P ๐‘…)))
123122adantl 277 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = (๐ถ ยทP (๐บ +P ๐‘…)))
124 distrprg 7600 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ P โˆง ๐น โˆˆ P โˆง ๐‘† โˆˆ P) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)))
12511, 14, 26, 124syl3anc 1248 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)))
126125adantr 276 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)))
127 distrprg 7600 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ P โˆง ๐บ โˆˆ P โˆง ๐‘… โˆˆ P) โ†’ (๐ถ ยทP (๐บ +P ๐‘…)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…)))
12811, 2, 6, 127syl3anc 1248 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ถ ยทP (๐บ +P ๐‘…)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…)))
129128adantr 276 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (๐ถ ยทP (๐บ +P ๐‘…)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…)))
130123, 126, 1293eqtr3d 2228 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…)))
131130oveq2d 5904 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
132121, 131eqtrd 2220 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
133132adantrl 478 . . . . . . . 8 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
134114, 133eqtrd 2220 . . . . . . 7 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
135 mulclpr 7584 . . . . . . . . . 10 ((๐ด โˆˆ P โˆง ๐น โˆˆ P) โ†’ (๐ด ยทP ๐น) โˆˆ P)
13635, 14, 135syl2anc 411 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (๐ด ยทP ๐น) โˆˆ P)
137136, 75, 118, 79, 81caov32d 6068 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น)))
138137adantr 276 . . . . . . 7 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น)))
13916, 13, 18, 79, 81caov12d 6069 . . . . . . . 8 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
140139adantr 276 . . . . . . 7 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
141134, 138, 1403eqtr3d 2228 . . . . . 6 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น)) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
142141oveq2d 5904 . . . . 5 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
14323, 87, 1423eqtr4rd 2231 . . . 4 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
144 addclpr 7549 . . . . . . 7 (((๐ด ยทP ๐น) โˆˆ P โˆง (๐ถ ยทP ๐‘†) โˆˆ P) โ†’ ((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) โˆˆ P)
145136, 118, 144syl2anc 411 . . . . . 6 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) โˆˆ P)
14610, 145, 75, 79, 81caov13d 6071 . . . . 5 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))))
147146adantr 276 . . . 4 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))))
148 addclpr 7549 . . . . . . 7 (((๐ด ยทP ๐บ) โˆˆ P โˆง (๐ท ยทP ๐‘†) โˆˆ P) โ†’ ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) โˆˆ P)
14937, 77, 148syl2anc 411 . . . . . 6 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) โˆˆ P)
150 addassprg 7591 . . . . . 6 (((๐ท ยทP ๐น) โˆˆ P โˆง ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) โˆˆ P โˆง ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)) โˆˆ P) โ†’ (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
15175, 149, 20, 150syl3anc 1248 . . . . 5 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
152151adantr 276 . . . 4 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
153143, 147, 1523eqtr3d 2228 . . 3 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
154 addclpr 7549 . . . . . . 7 ((๐‘ฅ โˆˆ P โˆง ๐‘ฆ โˆˆ P) โ†’ (๐‘ฅ +P ๐‘ฆ) โˆˆ P)
155154adantl 277 . . . . . 6 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง (๐‘ฅ โˆˆ P โˆง ๐‘ฆ โˆˆ P)) โ†’ (๐‘ฅ +P ๐‘ฆ) โˆˆ P)
156136, 118, 4, 79, 81, 8, 155caov4d 6072 . . . . 5 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…))) = (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…))))
157156oveq2d 5904 . . . 4 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))))
158157adantr 276 . . 3 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))))
15937, 77, 16, 79, 81, 18, 155caov42d 6074 . . . . 5 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†))))
160159oveq2d 5904 . . . 4 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†)))))
161160adantr 276 . . 3 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†)))))
162153, 158, 1613eqtr3d 2228 . 2 (((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โˆง ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…))) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†)))))
163162ex 115 1 ((((๐ด โˆˆ P โˆง ๐ต โˆˆ P) โˆง (๐ถ โˆˆ P โˆง ๐ท โˆˆ P)) โˆง ((๐น โˆˆ P โˆง ๐บ โˆˆ P) โˆง (๐‘… โˆˆ P โˆง ๐‘† โˆˆ P))) โ†’ (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†))))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 979   = wceq 1363   โˆˆ wcel 2158  (class class class)co 5888  Pcnp 7303   +P cpp 7305   ยทP cmp 7306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-eprel 4301  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-1o 6430  df-2o 6431  df-oadd 6434  df-omul 6435  df-er 6548  df-ec 6550  df-qs 6554  df-ni 7316  df-pli 7317  df-mi 7318  df-lti 7319  df-plpq 7356  df-mpq 7357  df-enq 7359  df-nqqs 7360  df-plqqs 7361  df-mqqs 7362  df-1nqqs 7363  df-rq 7364  df-ltnqqs 7365  df-enq0 7436  df-nq0 7437  df-0nq0 7438  df-plq0 7439  df-mq0 7440  df-inp 7478  df-iplp 7480  df-imp 7481
This theorem is referenced by:  mulcmpblnr  7753
  Copyright terms: Public domain W3C validator