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

Theorem axmulass 7871
Description: Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 7913. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
Assertion
Ref Expression
axmulass ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))

Proof of Theorem axmulass
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง ๐‘ค ๐‘ฃ ๐‘ข ๐‘“ ๐‘” โ„Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcnqs 7839 . 2 โ„‚ = ((R ร— R) / โ—ก E )
2 mulcnsrec 7841 . 2 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ]โ—ก E ยท [โŸจ๐‘ง, ๐‘คโŸฉ]โ—ก E ) = [โŸจ((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))), ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค))โŸฉ]โ—ก E )
3 mulcnsrec 7841 . 2 (((๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ([โŸจ๐‘ง, ๐‘คโŸฉ]โ—ก E ยท [โŸจ๐‘ฃ, ๐‘ขโŸฉ]โ—ก E ) = [โŸจ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))), ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))โŸฉ]โ—ก E )
4 mulcnsrec 7841 . 2 (((((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) โˆˆ R โˆง ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ([โŸจ((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))), ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค))โŸฉ]โ—ก E ยท [โŸจ๐‘ฃ, ๐‘ขโŸฉ]โ—ก E ) = [โŸจ((((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ฃ) +R (-1R ยทR (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ข))), ((((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ฃ) +R (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ข))โŸฉ]โ—ก E )
5 mulcnsrec 7841 . 2 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R โˆง ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)) โˆˆ R)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ]โ—ก E ยท [โŸจ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))), ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))โŸฉ]โ—ก E ) = [โŸจ((๐‘ฅ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R (-1R ยทR (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))))), ((๐‘ฆ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R (๐‘ฅ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))))โŸฉ]โ—ก E )
6 mulclsr 7752 . . . . 5 ((๐‘ฅ โˆˆ R โˆง ๐‘ง โˆˆ R) โ†’ (๐‘ฅ ยทR ๐‘ง) โˆˆ R)
7 m1r 7750 . . . . . 6 -1R โˆˆ R
8 mulclsr 7752 . . . . . 6 ((๐‘ฆ โˆˆ R โˆง ๐‘ค โˆˆ R) โ†’ (๐‘ฆ ยทR ๐‘ค) โˆˆ R)
9 mulclsr 7752 . . . . . 6 ((-1R โˆˆ R โˆง (๐‘ฆ ยทR ๐‘ค) โˆˆ R) โ†’ (-1R ยทR (๐‘ฆ ยทR ๐‘ค)) โˆˆ R)
107, 8, 9sylancr 414 . . . . 5 ((๐‘ฆ โˆˆ R โˆง ๐‘ค โˆˆ R) โ†’ (-1R ยทR (๐‘ฆ ยทR ๐‘ค)) โˆˆ R)
11 addclsr 7751 . . . . 5 (((๐‘ฅ ยทR ๐‘ง) โˆˆ R โˆง (-1R ยทR (๐‘ฆ ยทR ๐‘ค)) โˆˆ R) โ†’ ((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) โˆˆ R)
126, 10, 11syl2an 289 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ง โˆˆ R) โˆง (๐‘ฆ โˆˆ R โˆง ๐‘ค โˆˆ R)) โ†’ ((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) โˆˆ R)
1312an4s 588 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R)) โ†’ ((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) โˆˆ R)
14 mulclsr 7752 . . . . 5 ((๐‘ฆ โˆˆ R โˆง ๐‘ง โˆˆ R) โ†’ (๐‘ฆ ยทR ๐‘ง) โˆˆ R)
15 mulclsr 7752 . . . . 5 ((๐‘ฅ โˆˆ R โˆง ๐‘ค โˆˆ R) โ†’ (๐‘ฅ ยทR ๐‘ค) โˆˆ R)
16 addclsr 7751 . . . . 5 (((๐‘ฆ ยทR ๐‘ง) โˆˆ R โˆง (๐‘ฅ ยทR ๐‘ค) โˆˆ R) โ†’ ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) โˆˆ R)
1714, 15, 16syl2anr 290 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฆ โˆˆ R โˆง ๐‘ง โˆˆ R)) โ†’ ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) โˆˆ R)
1817an42s 589 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R)) โ†’ ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) โˆˆ R)
1913, 18jca 306 . 2 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R)) โ†’ (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) โˆˆ R โˆง ((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) โˆˆ R))
20 mulclsr 7752 . . . . 5 ((๐‘ง โˆˆ R โˆง ๐‘ฃ โˆˆ R) โ†’ (๐‘ง ยทR ๐‘ฃ) โˆˆ R)
21 mulclsr 7752 . . . . . 6 ((๐‘ค โˆˆ R โˆง ๐‘ข โˆˆ R) โ†’ (๐‘ค ยทR ๐‘ข) โˆˆ R)
22 mulclsr 7752 . . . . . 6 ((-1R โˆˆ R โˆง (๐‘ค ยทR ๐‘ข) โˆˆ R) โ†’ (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R)
237, 21, 22sylancr 414 . . . . 5 ((๐‘ค โˆˆ R โˆง ๐‘ข โˆˆ R) โ†’ (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R)
24 addclsr 7751 . . . . 5 (((๐‘ง ยทR ๐‘ฃ) โˆˆ R โˆง (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R) โ†’ ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R)
2520, 23, 24syl2an 289 . . . 4 (((๐‘ง โˆˆ R โˆง ๐‘ฃ โˆˆ R) โˆง (๐‘ค โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R)
2625an4s 588 . . 3 (((๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R)
27 mulclsr 7752 . . . . 5 ((๐‘ค โˆˆ R โˆง ๐‘ฃ โˆˆ R) โ†’ (๐‘ค ยทR ๐‘ฃ) โˆˆ R)
28 mulclsr 7752 . . . . 5 ((๐‘ง โˆˆ R โˆง ๐‘ข โˆˆ R) โ†’ (๐‘ง ยทR ๐‘ข) โˆˆ R)
29 addclsr 7751 . . . . 5 (((๐‘ค ยทR ๐‘ฃ) โˆˆ R โˆง (๐‘ง ยทR ๐‘ข) โˆˆ R) โ†’ ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)) โˆˆ R)
3027, 28, 29syl2anr 290 . . . 4 (((๐‘ง โˆˆ R โˆง ๐‘ข โˆˆ R) โˆง (๐‘ค โˆˆ R โˆง ๐‘ฃ โˆˆ R)) โ†’ ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)) โˆˆ R)
3130an42s 589 . . 3 (((๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)) โˆˆ R)
3226, 31jca 306 . 2 (((๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R โˆง ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)) โˆˆ R))
33 simp1l 1021 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ๐‘ฅ โˆˆ R)
34 simp2l 1023 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ๐‘ง โˆˆ R)
35 simp3l 1025 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ๐‘ฃ โˆˆ R)
3634, 35, 20syl2anc 411 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ง ยทR ๐‘ฃ) โˆˆ R)
37 mulclsr 7752 . . . . 5 ((๐‘ฅ โˆˆ R โˆง (๐‘ง ยทR ๐‘ฃ) โˆˆ R) โ†’ (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) โˆˆ R)
3833, 36, 37syl2anc 411 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) โˆˆ R)
39 simp2r 1024 . . . . . . 7 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ๐‘ค โˆˆ R)
40 simp3r 1026 . . . . . . 7 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ๐‘ข โˆˆ R)
4139, 40, 21syl2anc 411 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ค ยทR ๐‘ข) โˆˆ R)
427, 41, 22sylancr 414 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R)
43 mulclsr 7752 . . . . 5 ((๐‘ฅ โˆˆ R โˆง (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R) โ†’ (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R)
4433, 42, 43syl2anc 411 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R)
45 simp1r 1022 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ๐‘ฆ โˆˆ R)
4639, 35, 27syl2anc 411 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ค ยทR ๐‘ฃ) โˆˆ R)
47 mulclsr 7752 . . . . . 6 ((๐‘ฆ โˆˆ R โˆง (๐‘ค ยทR ๐‘ฃ) โˆˆ R) โ†’ (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) โˆˆ R)
4845, 46, 47syl2anc 411 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) โˆˆ R)
49 mulclsr 7752 . . . . 5 ((-1R โˆˆ R โˆง (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) โˆˆ R) โ†’ (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) โˆˆ R)
507, 48, 49sylancr 414 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) โˆˆ R)
51 addcomsrg 7753 . . . . 5 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (๐‘“ +R ๐‘”) = (๐‘” +R ๐‘“))
5251adantl 277 . . . 4 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R)) โ†’ (๐‘“ +R ๐‘”) = (๐‘” +R ๐‘“))
53 addasssrg 7754 . . . . 5 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ((๐‘“ +R ๐‘”) +R โ„Ž) = (๐‘“ +R (๐‘” +R โ„Ž)))
5453adantl 277 . . . 4 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R)) โ†’ ((๐‘“ +R ๐‘”) +R โ„Ž) = (๐‘“ +R (๐‘” +R โ„Ž)))
5534, 40, 28syl2anc 411 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ง ยทR ๐‘ข) โˆˆ R)
56 mulclsr 7752 . . . . . 6 ((๐‘ฆ โˆˆ R โˆง (๐‘ง ยทR ๐‘ข) โˆˆ R) โ†’ (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) โˆˆ R)
5745, 55, 56syl2anc 411 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) โˆˆ R)
58 mulclsr 7752 . . . . 5 ((-1R โˆˆ R โˆง (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) โˆˆ R) โ†’ (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) โˆˆ R)
597, 57, 58sylancr 414 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) โˆˆ R)
60 addclsr 7751 . . . . 5 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (๐‘“ +R ๐‘”) โˆˆ R)
6160adantl 277 . . . 4 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R)) โ†’ (๐‘“ +R ๐‘”) โˆˆ R)
6238, 44, 50, 52, 54, 59, 61caov42d 6060 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R ((-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))))) = (((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)))) +R ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))))
63 distrsrg 7757 . . . . 5 ((๐‘ฅ โˆˆ R โˆง (๐‘ง ยทR ๐‘ฃ) โˆˆ R โˆง (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R) โ†’ (๐‘ฅ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
6433, 36, 42, 63syl3anc 1238 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
65 distrsrg 7757 . . . . . . 7 ((๐‘ฆ โˆˆ R โˆง (๐‘ค ยทR ๐‘ฃ) โˆˆ R โˆง (๐‘ง ยทR ๐‘ข) โˆˆ R) โ†’ (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))) = ((๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))))
6645, 46, 55, 65syl3anc 1238 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))) = ((๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))))
6766oveq2d 5890 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)))) = (-1R ยทR ((๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)))))
687a1i 9 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ -1R โˆˆ R)
69 distrsrg 7757 . . . . . 6 ((-1R โˆˆ R โˆง (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) โˆˆ R โˆง (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) โˆˆ R) โ†’ (-1R ยทR ((๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)))) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)))))
7068, 48, 57, 69syl3anc 1238 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR ((๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)))) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)))))
7167, 70eqtrd 2210 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)))) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)))))
7264, 71oveq12d 5892 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ฅ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R (-1R ยทR (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))))) = (((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R ((-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))))))
73 mulcomsrg 7755 . . . . . . 7 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (๐‘“ ยทR ๐‘”) = (๐‘” ยทR ๐‘“))
7473adantl 277 . . . . . 6 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R)) โ†’ (๐‘“ ยทR ๐‘”) = (๐‘” ยทR ๐‘“))
75 distrsrg 7757 . . . . . . . . 9 ((โ„Ž โˆˆ R โˆง ๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (โ„Ž ยทR (๐‘“ +R ๐‘”)) = ((โ„Ž ยทR ๐‘“) +R (โ„Ž ยทR ๐‘”)))
76753coml 1210 . . . . . . . 8 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ (โ„Ž ยทR (๐‘“ +R ๐‘”)) = ((โ„Ž ยทR ๐‘“) +R (โ„Ž ยทR ๐‘”)))
77 simp3 999 . . . . . . . . 9 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ โ„Ž โˆˆ R)
78603adant3 1017 . . . . . . . . 9 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ (๐‘“ +R ๐‘”) โˆˆ R)
79 mulcomsrg 7755 . . . . . . . . 9 ((โ„Ž โˆˆ R โˆง (๐‘“ +R ๐‘”) โˆˆ R) โ†’ (โ„Ž ยทR (๐‘“ +R ๐‘”)) = ((๐‘“ +R ๐‘”) ยทR โ„Ž))
8077, 78, 79syl2anc 411 . . . . . . . 8 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ (โ„Ž ยทR (๐‘“ +R ๐‘”)) = ((๐‘“ +R ๐‘”) ยทR โ„Ž))
81 simp1 997 . . . . . . . . . 10 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ๐‘“ โˆˆ R)
82 mulcomsrg 7755 . . . . . . . . . 10 ((โ„Ž โˆˆ R โˆง ๐‘“ โˆˆ R) โ†’ (โ„Ž ยทR ๐‘“) = (๐‘“ ยทR โ„Ž))
8377, 81, 82syl2anc 411 . . . . . . . . 9 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ (โ„Ž ยทR ๐‘“) = (๐‘“ ยทR โ„Ž))
84 simp2 998 . . . . . . . . . 10 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ๐‘” โˆˆ R)
85 mulcomsrg 7755 . . . . . . . . . 10 ((โ„Ž โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (โ„Ž ยทR ๐‘”) = (๐‘” ยทR โ„Ž))
8677, 84, 85syl2anc 411 . . . . . . . . 9 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ (โ„Ž ยทR ๐‘”) = (๐‘” ยทR โ„Ž))
8783, 86oveq12d 5892 . . . . . . . 8 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ((โ„Ž ยทR ๐‘“) +R (โ„Ž ยทR ๐‘”)) = ((๐‘“ ยทR โ„Ž) +R (๐‘” ยทR โ„Ž)))
8876, 80, 873eqtr3d 2218 . . . . . . 7 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ((๐‘“ +R ๐‘”) ยทR โ„Ž) = ((๐‘“ ยทR โ„Ž) +R (๐‘” ยทR โ„Ž)))
8988adantl 277 . . . . . 6 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R)) โ†’ ((๐‘“ +R ๐‘”) ยทR โ„Ž) = ((๐‘“ ยทR โ„Ž) +R (๐‘” ยทR โ„Ž)))
90 mulasssrg 7756 . . . . . . 7 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ((๐‘“ ยทR ๐‘”) ยทR โ„Ž) = (๐‘“ ยทR (๐‘” ยทR โ„Ž)))
9190adantl 277 . . . . . 6 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R)) โ†’ ((๐‘“ ยทR ๐‘”) ยทR โ„Ž) = (๐‘“ ยทR (๐‘” ยทR โ„Ž)))
92 mulclsr 7752 . . . . . . 7 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (๐‘“ ยทR ๐‘”) โˆˆ R)
9392adantl 277 . . . . . 6 ((((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R)) โ†’ (๐‘“ ยทR ๐‘”) โˆˆ R)
9445, 39, 8syl2anc 411 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR ๐‘ค) โˆˆ R)
9574, 89, 91, 93, 33, 68, 34, 94, 35caovdilemd 6065 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ฃ) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ฃ))))
96 mulasssrg 7756 . . . . . . . 8 ((๐‘ฆ โˆˆ R โˆง ๐‘ค โˆˆ R โˆง ๐‘ฃ โˆˆ R) โ†’ ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ฃ) = (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)))
9745, 39, 35, 96syl3anc 1238 . . . . . . 7 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ฃ) = (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)))
9897oveq2d 5890 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ฃ)) = (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ))))
9998oveq2d 5890 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ฃ))) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)))))
10095, 99eqtrd 2210 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ฃ) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)))))
10174, 89, 91, 93, 45, 33, 34, 39, 40caovdilemd 6065 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ข) = ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข))))
102101oveq2d 5890 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ข)) = (-1R ยทR ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)))))
10393, 33, 41caovcld 6027 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R)
104 distrsrg 7757 . . . . . 6 ((-1R โˆˆ R โˆง (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) โˆˆ R โˆง (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R) โ†’ (-1R ยทR ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)))) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (-1R ยทR (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)))))
10568, 57, 103, 104syl3anc 1238 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)))) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (-1R ยทR (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)))))
10668, 33, 41, 74, 91caov12d 6055 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข))) = (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))
107106oveq2d 5890 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (-1R ยทR (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ข)))) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
108102, 105, 1073eqtrd 2214 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ข)) = ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
109100, 108oveq12d 5892 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ฃ) +R (-1R ยทR (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ข))) = (((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ฃ)))) +R ((-1R ยทR (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ข))) +R (๐‘ฅ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))))
11062, 72, 1093eqtr4rd 2221 . 2 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ฃ) +R (-1R ยทR (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ข))) = ((๐‘ฅ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R (-1R ยทR (๐‘ฆ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))))))
11193, 45, 36caovcld 6027 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) โˆˆ R)
11293, 45, 42caovcld 6027 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))) โˆˆ R)
11393, 33, 46caovcld 6027 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ)) โˆˆ R)
11493, 33, 55caovcld 6027 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) โˆˆ R)
115111, 112, 113, 52, 54, 114, 61caov42d 6060 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R ((๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)))) = (((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ))) +R ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))))
116 distrsrg 7757 . . . . 5 ((๐‘ฆ โˆˆ R โˆง (๐‘ง ยทR ๐‘ฃ) โˆˆ R โˆง (-1R ยทR (๐‘ค ยทR ๐‘ข)) โˆˆ R) โ†’ (๐‘ฆ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) = ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
11745, 36, 42, 116syl3anc 1238 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฆ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) = ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
118 distrsrg 7757 . . . . 5 ((๐‘ฅ โˆˆ R โˆง (๐‘ค ยทR ๐‘ฃ) โˆˆ R โˆง (๐‘ง ยทR ๐‘ข) โˆˆ R) โ†’ (๐‘ฅ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))) = ((๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข))))
11933, 46, 55, 118syl3anc 1238 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (๐‘ฅ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข))) = ((๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข))))
120117, 119oveq12d 5892 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ฆ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R (๐‘ฅ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)))) = (((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R ((๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)))))
12174, 89, 91, 93, 45, 33, 34, 39, 35caovdilemd 6065 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ฃ) = ((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ))))
12274, 89, 91, 93, 33, 68, 34, 94, 40caovdilemd 6065 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ข) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) +R (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ข))))
123 mulasssrg 7756 . . . . . . . . 9 ((๐‘ฆ โˆˆ R โˆง ๐‘ค โˆˆ R โˆง ๐‘ข โˆˆ R) โ†’ ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ข) = (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ข)))
12445, 39, 40, 123syl3anc 1238 . . . . . . . 8 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ข) = (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ข)))
125124oveq2d 5890 . . . . . . 7 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ข)) = (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ข))))
12668, 45, 41, 74, 91caov12d 6055 . . . . . . 7 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR (๐‘ฆ ยทR (๐‘ค ยทR ๐‘ข))) = (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))
127125, 126eqtrd 2210 . . . . . 6 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ข)) = (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))
128127oveq2d 5890 . . . . 5 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) +R (-1R ยทR ((๐‘ฆ ยทR ๐‘ค) ยทR ๐‘ข))) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
129122, 128eqtrd 2210 . . . 4 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ข) = ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข)))))
130121, 129oveq12d 5892 . . 3 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ฃ) +R (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ข)) = (((๐‘ฆ ยทR (๐‘ง ยทR ๐‘ฃ)) +R (๐‘ฅ ยทR (๐‘ค ยทR ๐‘ฃ))) +R ((๐‘ฅ ยทR (๐‘ง ยทR ๐‘ข)) +R (๐‘ฆ ยทR (-1R ยทR (๐‘ค ยทR ๐‘ข))))))
131115, 120, 1303eqtr4rd 2221 . 2 (((๐‘ฅ โˆˆ R โˆง ๐‘ฆ โˆˆ R) โˆง (๐‘ง โˆˆ R โˆง ๐‘ค โˆˆ R) โˆง (๐‘ฃ โˆˆ R โˆง ๐‘ข โˆˆ R)) โ†’ ((((๐‘ฆ ยทR ๐‘ง) +R (๐‘ฅ ยทR ๐‘ค)) ยทR ๐‘ฃ) +R (((๐‘ฅ ยทR ๐‘ง) +R (-1R ยทR (๐‘ฆ ยทR ๐‘ค))) ยทR ๐‘ข)) = ((๐‘ฆ ยทR ((๐‘ง ยทR ๐‘ฃ) +R (-1R ยทR (๐‘ค ยทR ๐‘ข)))) +R (๐‘ฅ ยทR ((๐‘ค ยทR ๐‘ฃ) +R (๐‘ง ยทR ๐‘ข)))))
1321, 2, 3, 4, 5, 19, 32, 110, 131ecoviass 6644 1 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148   E cep 4287  โ—กccnv 4625  (class class class)co 5874  Rcnr 7295  -1Rcm1r 7298   +R cplr 7299   ยทR cmr 7300  โ„‚cc 7808   ยท cmul 7815
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-eprel 4289  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-1o 6416  df-2o 6417  df-oadd 6420  df-omul 6421  df-er 6534  df-ec 6536  df-qs 6540  df-ni 7302  df-pli 7303  df-mi 7304  df-lti 7305  df-plpq 7342  df-mpq 7343  df-enq 7345  df-nqqs 7346  df-plqqs 7347  df-mqqs 7348  df-1nqqs 7349  df-rq 7350  df-ltnqqs 7351  df-enq0 7422  df-nq0 7423  df-0nq0 7424  df-plq0 7425  df-mq0 7426  df-inp 7464  df-i1p 7465  df-iplp 7466  df-imp 7467  df-enr 7724  df-nr 7725  df-plr 7726  df-mr 7727  df-m1r 7731  df-c 7816  df-mul 7822
This theorem is referenced by:  rereceu  7887  recriota  7888
  Copyright terms: Public domain W3C validator