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

Theorem distrnq0 7458
Description: Multiplication of nonnegative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.)
Assertion
Ref Expression
distrnq0 ((๐ด โˆˆ Q0 โˆง ๐ต โˆˆ Q0 โˆง ๐ถ โˆˆ Q0) โ†’ (๐ด ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ)))

Proof of Theorem distrnq0
Dummy variables ๐‘ข ๐‘ฃ ๐‘ค ๐‘ฅ ๐‘ฆ ๐‘ง ๐‘“ ๐‘” โ„Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nq0 7424 . . . 4 Q0 = ((ฯ‰ ร— N) / ~Q0 )
2 oveq1 5882 . . . . . . 7 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 = ๐ต โ†’ ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ) = (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))
32oveq2d 5891 . . . . . 6 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 = ๐ต โ†’ (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (๐ด ยทQ0 (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))
4 oveq2 5883 . . . . . . 7 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 = ๐ต โ†’ (๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) = (๐ด ยทQ0 ๐ต))
54oveq1d 5890 . . . . . 6 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 = ๐ต โ†’ ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))
63, 5eqeq12d 2192 . . . . 5 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 = ๐ต โ†’ ((๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) โ†” (๐ด ยทQ0 (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))))
76imbi2d 230 . . . 4 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 = ๐ต โ†’ ((๐ด โˆˆ Q0 โ†’ (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))) โ†” (๐ด โˆˆ Q0 โ†’ (๐ด ยทQ0 (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))))
8 oveq2 5883 . . . . . . 7 ([โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 = ๐ถ โ†’ (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ) = (๐ต +Q0 ๐ถ))
98oveq2d 5891 . . . . . 6 ([โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 = ๐ถ โ†’ (๐ด ยทQ0 (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (๐ด ยทQ0 (๐ต +Q0 ๐ถ)))
10 oveq2 5883 . . . . . . 7 ([โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 = ๐ถ โ†’ (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ) = (๐ด ยทQ0 ๐ถ))
1110oveq2d 5891 . . . . . 6 ([โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 = ๐ถ โ†’ ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ)))
129, 11eqeq12d 2192 . . . . 5 ([โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 = ๐ถ โ†’ ((๐ด ยทQ0 (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) โ†” (๐ด ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ))))
1312imbi2d 230 . . . 4 ([โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 = ๐ถ โ†’ ((๐ด โˆˆ Q0 โ†’ (๐ด ยทQ0 (๐ต +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))) โ†” (๐ด โˆˆ Q0 โ†’ (๐ด ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ)))))
14 oveq1 5882 . . . . . . . 8 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 = ๐ด โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))
15 oveq1 5882 . . . . . . . . 9 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 = ๐ด โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) = (๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ))
16 oveq1 5882 . . . . . . . . 9 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 = ๐ด โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ) = (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))
1715, 16oveq12d 5893 . . . . . . . 8 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 = ๐ด โ†’ (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))
1814, 17eqeq12d 2192 . . . . . . 7 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 = ๐ด โ†’ (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) โ†” (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))))
1918imbi2d 230 . . . . . 6 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 = ๐ด โ†’ ((((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))) โ†” (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))))
20 an42 587 . . . . . . . . . . . 12 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†” ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)))
2120anbi2i 457 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰))) โ†” ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))))
22 3anass 982 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†” ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰))))
23 3anass 982 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†” ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))))
2421, 22, 233bitr4i 212 . . . . . . . . . 10 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†” ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)))
25 pinn 7308 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ N โ†’ ๐‘ฆ โˆˆ ฯ‰)
26 nnmcl 6482 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ ฯ‰ โˆง ๐‘ฅ โˆˆ ฯ‰) โ†’ (๐‘ฆ ยทo ๐‘ฅ) โˆˆ ฯ‰)
2725, 26sylan 283 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ N โˆง ๐‘ฅ โˆˆ ฯ‰) โ†’ (๐‘ฆ ยทo ๐‘ฅ) โˆˆ ฯ‰)
2827ancoms 268 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โ†’ (๐‘ฆ ยทo ๐‘ฅ) โˆˆ ฯ‰)
29 pinn 7308 . . . . . . . . . . . . 13 (๐‘ข โˆˆ N โ†’ ๐‘ข โˆˆ ฯ‰)
30 nnmcl 6482 . . . . . . . . . . . . 13 ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ ฯ‰) โ†’ (๐‘ง ยทo ๐‘ข) โˆˆ ฯ‰)
3129, 30sylan2 286 . . . . . . . . . . . 12 ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โ†’ (๐‘ง ยทo ๐‘ข) โˆˆ ฯ‰)
32 pinn 7308 . . . . . . . . . . . . 13 (๐‘ค โˆˆ N โ†’ ๐‘ค โˆˆ ฯ‰)
33 nnmcl 6482 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ ฯ‰) โ†’ (๐‘ค ยทo ๐‘ฃ) โˆˆ ฯ‰)
3432, 33sylan 283 . . . . . . . . . . . 12 ((๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰) โ†’ (๐‘ค ยทo ๐‘ฃ) โˆˆ ฯ‰)
35 nndi 6487 . . . . . . . . . . . 12 (((๐‘ฆ ยทo ๐‘ฅ) โˆˆ ฯ‰ โˆง (๐‘ง ยทo ๐‘ข) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ฃ) โˆˆ ฯ‰) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) = (((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ค ยทo ๐‘ฃ))))
3628, 31, 34, 35syl3an 1280 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) = (((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ค ยทo ๐‘ฃ))))
37 simp1r 1022 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ฆ โˆˆ N)
38 simp1l 1021 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ฅ โˆˆ ฯ‰)
39313ad2ant2 1019 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ง ยทo ๐‘ข) โˆˆ ฯ‰)
40343ad2ant3 1020 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ค ยทo ๐‘ฃ) โˆˆ ฯ‰)
41 nnacl 6481 . . . . . . . . . . . . 13 (((๐‘ง ยทo ๐‘ข) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ฃ) โˆˆ ฯ‰) โ†’ ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰)
4239, 40, 41syl2anc 411 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰)
43 nnmass 6488 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ ฯ‰ โˆง ๐‘ฅ โˆˆ ฯ‰ โˆง ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) = (๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))))
4425, 43syl3an1 1271 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ N โˆง ๐‘ฅ โˆˆ ฯ‰ โˆง ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) = (๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))))
4537, 38, 42, 44syl3anc 1238 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) = (๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))))
46 nnmcom 6490 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ฅ ยทo ๐‘ฆ) = (๐‘ฆ ยทo ๐‘ฅ))
4725, 46sylan2 286 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โ†’ (๐‘ฅ ยทo ๐‘ฆ) = (๐‘ฆ ยทo ๐‘ฅ))
4847oveq1d 5890 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โ†’ ((๐‘ฅ ยทo ๐‘ฆ) ยทo (๐‘ง ยทo ๐‘ข)) = ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)))
4948adantr 276 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ฅ ยทo ๐‘ฆ) ยทo (๐‘ง ยทo ๐‘ข)) = ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)))
50 simpll 527 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ๐‘ฅ โˆˆ ฯ‰)
5125ad2antlr 489 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ๐‘ฆ โˆˆ ฯ‰)
52 simprl 529 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ๐‘ง โˆˆ ฯ‰)
53 nnmcom 6490 . . . . . . . . . . . . . . . 16 ((๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰) โ†’ (๐‘“ ยทo ๐‘”) = (๐‘” ยทo ๐‘“))
5453adantl 277 . . . . . . . . . . . . . . 15 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰)) โ†’ (๐‘“ ยทo ๐‘”) = (๐‘” ยทo ๐‘“))
55 nnmass 6488 . . . . . . . . . . . . . . . 16 ((๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰ โˆง โ„Ž โˆˆ ฯ‰) โ†’ ((๐‘“ ยทo ๐‘”) ยทo โ„Ž) = (๐‘“ ยทo (๐‘” ยทo โ„Ž)))
5655adantl 277 . . . . . . . . . . . . . . 15 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰ โˆง โ„Ž โˆˆ ฯ‰)) โ†’ ((๐‘“ ยทo ๐‘”) ยทo โ„Ž) = (๐‘“ ยทo (๐‘” ยทo โ„Ž)))
57 simprr 531 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ๐‘ข โˆˆ N)
5857, 29syl 14 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ๐‘ข โˆˆ ฯ‰)
59 nnmcl 6482 . . . . . . . . . . . . . . . 16 ((๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰) โ†’ (๐‘“ ยทo ๐‘”) โˆˆ ฯ‰)
6059adantl 277 . . . . . . . . . . . . . . 15 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰)) โ†’ (๐‘“ ยทo ๐‘”) โˆˆ ฯ‰)
6150, 51, 52, 54, 56, 58, 60caov4d 6059 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ฅ ยทo ๐‘ฆ) ยทo (๐‘ง ยทo ๐‘ข)) = ((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)))
6249, 61eqtr3d 2212 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)) = ((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)))
63623adant3 1017 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)) = ((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)))
6425ad2antlr 489 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ฆ โˆˆ ฯ‰)
65 simpll 527 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ฅ โˆˆ ฯ‰)
66 simprl 529 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ค โˆˆ N)
6766, 32syl 14 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ค โˆˆ ฯ‰)
6853adantl 277 . . . . . . . . . . . . . 14 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰)) โ†’ (๐‘“ ยทo ๐‘”) = (๐‘” ยทo ๐‘“))
6955adantl 277 . . . . . . . . . . . . . 14 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰ โˆง โ„Ž โˆˆ ฯ‰)) โ†’ ((๐‘“ ยทo ๐‘”) ยทo โ„Ž) = (๐‘“ ยทo (๐‘” ยทo โ„Ž)))
70 simprr 531 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ฃ โˆˆ ฯ‰)
7159adantl 277 . . . . . . . . . . . . . 14 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰)) โ†’ (๐‘“ ยทo ๐‘”) โˆˆ ฯ‰)
7264, 65, 67, 68, 69, 70, 71caov4d 6059 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ค ยทo ๐‘ฃ)) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ)))
73723adant2 1016 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ค ยทo ๐‘ฃ)) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ)))
7463, 73oveq12d 5893 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ง ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ฅ) ยทo (๐‘ค ยทo ๐‘ฃ))) = (((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))))
7536, 45, 743eqtr3d 2218 . . . . . . . . . 10 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))) = (((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))))
7624, 75sylbir 135 . . . . . . . . 9 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))) = (((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))))
7737, 25syl 14 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ฆ โˆˆ ฯ‰)
78 mulpiord 7316 . . . . . . . . . . . . . . . 16 ((๐‘ค โˆˆ N โˆง ๐‘ข โˆˆ N) โ†’ (๐‘ค ยทN ๐‘ข) = (๐‘ค ยทo ๐‘ข))
7978ancoms 268 . . . . . . . . . . . . . . 15 ((๐‘ข โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ค ยทN ๐‘ข) = (๐‘ค ยทo ๐‘ข))
8079ad2ant2lr 510 . . . . . . . . . . . . . 14 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ค ยทN ๐‘ข) = (๐‘ค ยทo ๐‘ข))
81803adant1 1015 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ค ยทN ๐‘ข) = (๐‘ค ยทo ๐‘ข))
82663adant2 1016 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ค โˆˆ N)
83573adant3 1017 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ข โˆˆ N)
84 mulclpi 7327 . . . . . . . . . . . . . . 15 ((๐‘ค โˆˆ N โˆง ๐‘ข โˆˆ N) โ†’ (๐‘ค ยทN ๐‘ข) โˆˆ N)
8582, 83, 84syl2anc 411 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ค ยทN ๐‘ข) โˆˆ N)
86 pinn 7308 . . . . . . . . . . . . . 14 ((๐‘ค ยทN ๐‘ข) โˆˆ N โ†’ (๐‘ค ยทN ๐‘ข) โˆˆ ฯ‰)
8785, 86syl 14 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ค ยทN ๐‘ข) โˆˆ ฯ‰)
8881, 87eqeltrrd 2255 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ค ยทo ๐‘ข) โˆˆ ฯ‰)
89 nnmass 6488 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ข) โˆˆ ฯ‰) โ†’ ((๐‘ฆ ยทo ๐‘ฆ) ยทo (๐‘ค ยทo ๐‘ข)) = (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))))
9077, 77, 88, 89syl3anc 1238 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฆ) ยทo (๐‘ค ยทo ๐‘ข)) = (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))))
9182, 32syl 14 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ค โˆˆ ฯ‰)
9253adantl 277 . . . . . . . . . . . 12 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰)) โ†’ (๐‘“ ยทo ๐‘”) = (๐‘” ยทo ๐‘“))
9355adantl 277 . . . . . . . . . . . 12 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰ โˆง โ„Ž โˆˆ ฯ‰)) โ†’ ((๐‘“ ยทo ๐‘”) ยทo โ„Ž) = (๐‘“ ยทo (๐‘” ยทo โ„Ž)))
9483, 29syl 14 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ๐‘ข โˆˆ ฯ‰)
9559adantl 277 . . . . . . . . . . . 12 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โˆง (๐‘“ โˆˆ ฯ‰ โˆง ๐‘” โˆˆ ฯ‰)) โ†’ (๐‘“ ยทo ๐‘”) โˆˆ ฯ‰)
9677, 77, 91, 92, 93, 94, 95caov4d 6059 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ฆ ยทo ๐‘ฆ) ยทo (๐‘ค ยทo ๐‘ข)) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข)))
9790, 96eqtr3d 2212 . . . . . . . . . 10 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข)))
9824, 97sylbir 135 . . . . . . . . 9 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข)))
99 opeq12 3781 . . . . . . . . . 10 (((๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))) = (((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))) โˆง (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))) โ†’ โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ = โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ)
10099eceq1d 6571 . . . . . . . . 9 (((๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))) = (((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))) โˆง (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))) = ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))) โ†’ [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 = [โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ] ~Q0 )
10176, 98, 100syl2anc 411 . . . . . . . 8 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 = [โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ] ~Q0 )
102 addnnnq0 7448 . . . . . . . . . . . 12 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ) = [โŸจ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)), (๐‘ค ยทo ๐‘ข)โŸฉ] ~Q0 )
103102oveq2d 5891 . . . . . . . . . . 11 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)), (๐‘ค ยทo ๐‘ข)โŸฉ] ~Q0 ))
104103adantl 277 . . . . . . . . . 10 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)), (๐‘ค ยทo ๐‘ข)โŸฉ] ~Q0 ))
10531, 34, 41syl2an 289 . . . . . . . . . . . . 13 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N) โˆง (๐‘ค โˆˆ N โˆง ๐‘ฃ โˆˆ ฯ‰)) โ†’ ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰)
106105an42s 589 . . . . . . . . . . . 12 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰)
10784ad2ant2l 508 . . . . . . . . . . . . 13 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐‘ค ยทN ๐‘ข) โˆˆ N)
10878eleq1d 2246 . . . . . . . . . . . . . 14 ((๐‘ค โˆˆ N โˆง ๐‘ข โˆˆ N) โ†’ ((๐‘ค ยทN ๐‘ข) โˆˆ N โ†” (๐‘ค ยทo ๐‘ข) โˆˆ N))
109108ad2ant2l 508 . . . . . . . . . . . . 13 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ค ยทN ๐‘ข) โˆˆ N โ†” (๐‘ค ยทo ๐‘ข) โˆˆ N))
110107, 109mpbid 147 . . . . . . . . . . . 12 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐‘ค ยทo ๐‘ข) โˆˆ N)
111106, 110jca 306 . . . . . . . . . . 11 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N))
112 mulnnnq0 7449 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)), (๐‘ค ยทo ๐‘ข)โŸฉ] ~Q0 ) = [โŸจ(๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))), (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))โŸฉ] ~Q0 )
113 nnmcl 6482 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ ฯ‰ โˆง ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰) โ†’ (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰)
114 simpl 109 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N) โ†’ ๐‘ฆ โˆˆ N)
115 mulpiord 7316 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N) โ†’ (๐‘ฆ ยทN (๐‘ค ยทo ๐‘ข)) = (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))
116 mulclpi 7327 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N) โ†’ (๐‘ฆ ยทN (๐‘ค ยทo ๐‘ข)) โˆˆ N)
117115, 116eqeltrrd 2255 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N) โ†’ (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N)
118114, 117jca 306 . . . . . . . . . . . . . . . 16 ((๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N) โ†’ (๐‘ฆ โˆˆ N โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N))
119113, 118anim12i 338 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ ฯ‰ โˆง ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰) โˆง (๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N)) โ†’ ((๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ โˆˆ N โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N)))
120 an12 561 . . . . . . . . . . . . . . . 16 (((๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ โˆˆ N โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N)) โ†” (๐‘ฆ โˆˆ N โˆง ((๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N)))
121 3anass 982 . . . . . . . . . . . . . . . 16 ((๐‘ฆ โˆˆ N โˆง (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N) โ†” (๐‘ฆ โˆˆ N โˆง ((๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N)))
122120, 121bitr4i 187 . . . . . . . . . . . . . . 15 (((๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ โˆˆ N โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N)) โ†” (๐‘ฆ โˆˆ N โˆง (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N))
123119, 122sylib 122 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ ฯ‰ โˆง ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰) โˆง (๐‘ฆ โˆˆ N โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N)) โ†’ (๐‘ฆ โˆˆ N โˆง (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N))
124123an4s 588 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N)) โ†’ (๐‘ฆ โˆˆ N โˆง (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N))
125 mulcanenq0ec 7444 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ N โˆง (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)) โˆˆ N) โ†’ [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 = [โŸจ(๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))), (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))โŸฉ] ~Q0 )
126124, 125syl 14 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N)) โ†’ [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 = [โŸจ(๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ))), (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข))โŸฉ] ~Q0 )
127112, 126eqtr4d 2213 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)) โˆˆ ฯ‰ โˆง (๐‘ค ยทo ๐‘ข) โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)), (๐‘ค ยทo ๐‘ข)โŸฉ] ~Q0 ) = [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 )
128111, 127sylan2 286 . . . . . . . . . 10 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)), (๐‘ค ยทo ๐‘ข)โŸฉ] ~Q0 ) = [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 )
129104, 128eqtrd 2210 . . . . . . . . 9 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง ((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 )
1301293impb 1199 . . . . . . . 8 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = [โŸจ(๐‘ฆ ยทo (๐‘ฅ ยทo ((๐‘ง ยทo ๐‘ข) +o (๐‘ค ยทo ๐‘ฃ)))), (๐‘ฆ ยทo (๐‘ฆ ยทo (๐‘ค ยทo ๐‘ข)))โŸฉ] ~Q0 )
131 mulnnnq0 7449 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) = [โŸจ(๐‘ฅ ยทo ๐‘ง), (๐‘ฆ ยทo ๐‘ค)โŸฉ] ~Q0 )
132 mulnnnq0 7449 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ) = [โŸจ(๐‘ฅ ยทo ๐‘ฃ), (๐‘ฆ ยทo ๐‘ข)โŸฉ] ~Q0 )
133131, 132oveqan12d 5894 . . . . . . . . . 10 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N)) โˆง ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))) โ†’ (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ([โŸจ(๐‘ฅ ยทo ๐‘ง), (๐‘ฆ ยทo ๐‘ค)โŸฉ] ~Q0 +Q0 [โŸจ(๐‘ฅ ยทo ๐‘ฃ), (๐‘ฆ ยทo ๐‘ข)โŸฉ] ~Q0 ))
134 nnmcl 6482 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ง โˆˆ ฯ‰) โ†’ (๐‘ฅ ยทo ๐‘ง) โˆˆ ฯ‰)
135 mulpiord 7316 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ฆ ยทN ๐‘ค) = (๐‘ฆ ยทo ๐‘ค))
136 mulclpi 7327 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ฆ ยทN ๐‘ค) โˆˆ N)
137135, 136eqeltrrd 2255 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ฆ ยทo ๐‘ค) โˆˆ N)
138134, 137anim12i 338 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ง โˆˆ ฯ‰) โˆง (๐‘ฆ โˆˆ N โˆง ๐‘ค โˆˆ N)) โ†’ ((๐‘ฅ ยทo ๐‘ง) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo ๐‘ค) โˆˆ N))
139138an4s 588 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N)) โ†’ ((๐‘ฅ ยทo ๐‘ง) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo ๐‘ค) โˆˆ N))
140 nnmcl 6482 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ ฯ‰) โ†’ (๐‘ฅ ยทo ๐‘ฃ) โˆˆ ฯ‰)
141 mulpiord 7316 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ N โˆง ๐‘ข โˆˆ N) โ†’ (๐‘ฆ ยทN ๐‘ข) = (๐‘ฆ ยทo ๐‘ข))
142 mulclpi 7327 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ N โˆง ๐‘ข โˆˆ N) โ†’ (๐‘ฆ ยทN ๐‘ข) โˆˆ N)
143141, 142eqeltrrd 2255 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ N โˆง ๐‘ข โˆˆ N) โ†’ (๐‘ฆ ยทo ๐‘ข) โˆˆ N)
144140, 143anim12i 338 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฃ โˆˆ ฯ‰) โˆง (๐‘ฆ โˆˆ N โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ฅ ยทo ๐‘ฃ) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo ๐‘ข) โˆˆ N))
145144an4s 588 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ((๐‘ฅ ยทo ๐‘ฃ) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo ๐‘ข) โˆˆ N))
146 addnnnq0 7448 . . . . . . . . . . 11 ((((๐‘ฅ ยทo ๐‘ง) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo ๐‘ค) โˆˆ N) โˆง ((๐‘ฅ ยทo ๐‘ฃ) โˆˆ ฯ‰ โˆง (๐‘ฆ ยทo ๐‘ข) โˆˆ N)) โ†’ ([โŸจ(๐‘ฅ ยทo ๐‘ง), (๐‘ฆ ยทo ๐‘ค)โŸฉ] ~Q0 +Q0 [โŸจ(๐‘ฅ ยทo ๐‘ฃ), (๐‘ฆ ยทo ๐‘ข)โŸฉ] ~Q0 ) = [โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ] ~Q0 )
147139, 145, 146syl2an 289 . . . . . . . . . 10 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N)) โˆง ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))) โ†’ ([โŸจ(๐‘ฅ ยทo ๐‘ง), (๐‘ฆ ยทo ๐‘ค)โŸฉ] ~Q0 +Q0 [โŸจ(๐‘ฅ ยทo ๐‘ฃ), (๐‘ฆ ยทo ๐‘ข)โŸฉ] ~Q0 ) = [โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ] ~Q0 )
148133, 147eqtrd 2210 . . . . . . . . 9 ((((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N)) โˆง ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N))) โ†’ (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = [โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ] ~Q0 )
1491483impdi 1293 . . . . . . . 8 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = [โŸจ(((๐‘ฅ ยทo ๐‘ง) ยทo (๐‘ฆ ยทo ๐‘ข)) +o ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฅ ยทo ๐‘ฃ))), ((๐‘ฆ ยทo ๐‘ค) ยทo (๐‘ฆ ยทo ๐‘ข))โŸฉ] ~Q0 )
150101, 130, 1493eqtr4d 2220 . . . . . . 7 (((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โˆง (๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )))
1511503expib 1206 . . . . . 6 ((๐‘ฅ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ N) โ†’ (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = (([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 ([โŸจ๐‘ฅ, ๐‘ฆโŸฉ] ~Q0 ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))))
1521, 19, 151ecoptocl 6622 . . . . 5 (๐ด โˆˆ Q0 โ†’ (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))))
153152com12 30 . . . 4 (((๐‘ง โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ N) โˆง (๐‘ฃ โˆˆ ฯ‰ โˆง ๐‘ข โˆˆ N)) โ†’ (๐ด โˆˆ Q0 โ†’ (๐ด ยทQ0 ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 +Q0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 )) = ((๐ด ยทQ0 [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q0 ) +Q0 (๐ด ยทQ0 [โŸจ๐‘ฃ, ๐‘ขโŸฉ] ~Q0 ))))
1541, 7, 13, 1532ecoptocl 6623 . . 3 ((๐ต โˆˆ Q0 โˆง ๐ถ โˆˆ Q0) โ†’ (๐ด โˆˆ Q0 โ†’ (๐ด ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ))))
155154com12 30 . 2 (๐ด โˆˆ Q0 โ†’ ((๐ต โˆˆ Q0 โˆง ๐ถ โˆˆ Q0) โ†’ (๐ด ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ))))
1561553impib 1201 1 ((๐ด โˆˆ Q0 โˆง ๐ต โˆˆ Q0 โˆง ๐ถ โˆˆ Q0) โ†’ (๐ด ยทQ0 (๐ต +Q0 ๐ถ)) = ((๐ด ยทQ0 ๐ต) +Q0 (๐ด ยทQ0 ๐ถ)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โŸจcop 3596  ฯ‰com 4590  (class class class)co 5875   +o coa 6414   ยทo comu 6415  [cec 6533  Ncnpi 7271   ยทN cmi 7273   ~Q0 ceq0 7285  Q0cnq0 7286   +Q0 cplq0 7288   ยทQ0 cmq0 7289
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 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
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 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-irdg 6371  df-oadd 6421  df-omul 6422  df-er 6535  df-ec 6537  df-qs 6541  df-ni 7303  df-mi 7305  df-enq0 7423  df-nq0 7424  df-plq0 7426  df-mq0 7427
This theorem is referenced by:  distnq0r  7462
  Copyright terms: Public domain W3C validator