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

Theorem mulcmpblnrlem 11069
Description: Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.)
Assertion
Ref Expression
mulcmpblnrlem (((๐ด +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 mulcmpblnrlem
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7419 . . . . . . . . 9 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = ((๐ต +P ๐ถ) ยทP ๐น))
2 distrpr 11027 . . . . . . . . . 10 (๐น ยทP (๐ด +P ๐ท)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท))
3 mulcompr 11022 . . . . . . . . . 10 ((๐ด +P ๐ท) ยทP ๐น) = (๐น ยทP (๐ด +P ๐ท))
4 mulcompr 11022 . . . . . . . . . . 11 (๐ด ยทP ๐น) = (๐น ยทP ๐ด)
5 mulcompr 11022 . . . . . . . . . . 11 (๐ท ยทP ๐น) = (๐น ยทP ๐ท)
64, 5oveq12i 7424 . . . . . . . . . 10 ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท))
72, 3, 63eqtr4i 2769 . . . . . . . . 9 ((๐ด +P ๐ท) ยทP ๐น) = ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น))
8 distrpr 11027 . . . . . . . . . 10 (๐น ยทP (๐ต +P ๐ถ)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ))
9 mulcompr 11022 . . . . . . . . . 10 ((๐ต +P ๐ถ) ยทP ๐น) = (๐น ยทP (๐ต +P ๐ถ))
10 mulcompr 11022 . . . . . . . . . . 11 (๐ต ยทP ๐น) = (๐น ยทP ๐ต)
11 mulcompr 11022 . . . . . . . . . . 11 (๐ถ ยทP ๐น) = (๐น ยทP ๐ถ)
1210, 11oveq12i 7424 . . . . . . . . . 10 ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ))
138, 9, 123eqtr4i 2769 . . . . . . . . 9 ((๐ต +P ๐ถ) ยทP ๐น) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น))
141, 7, 133eqtr3g 2794 . . . . . . . 8 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)))
1514oveq1d 7427 . . . . . . 7 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)))
16 addasspr 11021 . . . . . . . 8 (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)))
17 oveq2 7420 . . . . . . . . . 10 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = (๐ถ ยทP (๐บ +P ๐‘…)))
18 distrpr 11027 . . . . . . . . . 10 (๐ถ ยทP (๐น +P ๐‘†)) = ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))
19 distrpr 11027 . . . . . . . . . 10 (๐ถ ยทP (๐บ +P ๐‘…)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))
2017, 18, 193eqtr3g 2794 . . . . . . . . 9 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…)))
2120oveq2d 7428 . . . . . . . 8 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
2216, 21eqtrid 2783 . . . . . . 7 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
2315, 22sylan9eq 2791 . . . . . 6 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
24 ovex 7445 . . . . . . 7 (๐ด ยทP ๐น) โˆˆ V
25 ovex 7445 . . . . . . 7 (๐ท ยทP ๐น) โˆˆ V
26 ovex 7445 . . . . . . 7 (๐ถ ยทP ๐‘†) โˆˆ V
27 addcompr 11020 . . . . . . 7 (๐‘ฅ +P ๐‘ฆ) = (๐‘ฆ +P ๐‘ฅ)
28 addasspr 11021 . . . . . . 7 ((๐‘ฅ +P ๐‘ฆ) +P ๐‘ง) = (๐‘ฅ +P (๐‘ฆ +P ๐‘ง))
2924, 25, 26, 27, 28caov32 7638 . . . . . 6 (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))
30 ovex 7445 . . . . . . 7 (๐ต ยทP ๐น) โˆˆ V
31 ovex 7445 . . . . . . 7 (๐ถ ยทP ๐บ) โˆˆ V
32 ovex 7445 . . . . . . 7 (๐ถ ยทP ๐‘…) โˆˆ V
3330, 31, 32, 27, 28caov12 7639 . . . . . 6 ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))
3423, 29, 333eqtr3g 2794 . . . . 5 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น)) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
3534oveq2d 7428 . . . 4 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
36 oveq2 7420 . . . . . . . . . . 11 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = (๐ท ยทP (๐บ +P ๐‘…)))
37 distrpr 11027 . . . . . . . . . . 11 (๐ท ยทP (๐น +P ๐‘†)) = ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))
38 distrpr 11027 . . . . . . . . . . 11 (๐ท ยทP (๐บ +P ๐‘…)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))
3936, 37, 383eqtr3g 2794 . . . . . . . . . 10 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
4039oveq2d 7428 . . . . . . . . 9 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
41 addasspr 11021 . . . . . . . . 9 (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
4240, 41eqtr4di 2789 . . . . . . . 8 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
43 oveq1 7419 . . . . . . . . . 10 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ต +P ๐ถ) ยทP ๐บ))
44 distrpr 11027 . . . . . . . . . . 11 (๐บ ยทP (๐ด +P ๐ท)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท))
45 mulcompr 11022 . . . . . . . . . . 11 ((๐ด +P ๐ท) ยทP ๐บ) = (๐บ ยทP (๐ด +P ๐ท))
46 mulcompr 11022 . . . . . . . . . . . 12 (๐ด ยทP ๐บ) = (๐บ ยทP ๐ด)
47 mulcompr 11022 . . . . . . . . . . . 12 (๐ท ยทP ๐บ) = (๐บ ยทP ๐ท)
4846, 47oveq12i 7424 . . . . . . . . . . 11 ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท))
4944, 45, 483eqtr4i 2769 . . . . . . . . . 10 ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ))
50 distrpr 11027 . . . . . . . . . . 11 (๐บ ยทP (๐ต +P ๐ถ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ))
51 mulcompr 11022 . . . . . . . . . . 11 ((๐ต +P ๐ถ) ยทP ๐บ) = (๐บ ยทP (๐ต +P ๐ถ))
52 mulcompr 11022 . . . . . . . . . . . 12 (๐ต ยทP ๐บ) = (๐บ ยทP ๐ต)
53 mulcompr 11022 . . . . . . . . . . . 12 (๐ถ ยทP ๐บ) = (๐บ ยทP ๐ถ)
5452, 53oveq12i 7424 . . . . . . . . . . 11 ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ))
5550, 51, 543eqtr4i 2769 . . . . . . . . . 10 ((๐ต +P ๐ถ) ยทP ๐บ) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ))
5643, 49, 553eqtr3g 2794 . . . . . . . . 9 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)))
5756oveq1d 7427 . . . . . . . 8 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
5842, 57sylan9eqr 2793 . . . . . . 7 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
59 ovex 7445 . . . . . . . 8 (๐ด ยทP ๐บ) โˆˆ V
60 ovex 7445 . . . . . . . 8 (๐ท ยทP ๐‘†) โˆˆ V
6159, 25, 60, 27, 28caov12 7639 . . . . . . 7 ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)))
62 ovex 7445 . . . . . . . 8 (๐ต ยทP ๐บ) โˆˆ V
63 ovex 7445 . . . . . . . 8 (๐ท ยทP ๐‘…) โˆˆ V
6462, 31, 63, 27, 28caov32 7638 . . . . . . 7 (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ))
6558, 61, 643eqtr3g 2794 . . . . . 6 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)))
6665oveq1d 7427 . . . . 5 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
67 addasspr 11021 . . . . 5 ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
6866, 67eqtrdi 2787 . . . 4 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
6935, 68eqtr4d 2774 . . 3 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
70 ovex 7445 . . . 4 ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) โˆˆ V
71 ovex 7445 . . . 4 ((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) โˆˆ V
7270, 71, 25, 27, 28caov13 7641 . . 3 (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
73 addasspr 11021 . . 3 (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
7469, 72, 733eqtr3g 2794 . 2 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))))
7524, 26, 62, 27, 28, 63caov4 7642 . . 3 (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…))) = (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))
7675oveq2i 7423 . 2 ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…))))
7759, 60, 30, 27, 28, 32caov42 7644 . . 3 (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†)))
7877oveq2i 7423 . 2 ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†))))
7974, 76, 783eqtr3g 2794 1 (((๐ด +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 setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1540  (class class class)co 7412   +P cpp 10860   ยทP cmp 10861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9640
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-oadd 8474  df-omul 8475  df-er 8707  df-ni 10871  df-pli 10872  df-mi 10873  df-lti 10874  df-plpq 10907  df-mpq 10908  df-ltpq 10909  df-enq 10910  df-nq 10911  df-erq 10912  df-plq 10913  df-mq 10914  df-1nq 10915  df-rq 10916  df-ltnq 10917  df-np 10980  df-plp 10982  df-mp 10983
This theorem is referenced by:  mulcmpblnr  11070
  Copyright terms: Public domain W3C validator