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

Theorem mulcmpblnrlem 11065
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 7416 . . . . . . . . 9 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด +P ๐ท) ยทP ๐น) = ((๐ต +P ๐ถ) ยทP ๐น))
2 distrpr 11023 . . . . . . . . . 10 (๐น ยทP (๐ด +P ๐ท)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท))
3 mulcompr 11018 . . . . . . . . . 10 ((๐ด +P ๐ท) ยทP ๐น) = (๐น ยทP (๐ด +P ๐ท))
4 mulcompr 11018 . . . . . . . . . . 11 (๐ด ยทP ๐น) = (๐น ยทP ๐ด)
5 mulcompr 11018 . . . . . . . . . . 11 (๐ท ยทP ๐น) = (๐น ยทP ๐ท)
64, 5oveq12i 7421 . . . . . . . . . 10 ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) = ((๐น ยทP ๐ด) +P (๐น ยทP ๐ท))
72, 3, 63eqtr4i 2771 . . . . . . . . 9 ((๐ด +P ๐ท) ยทP ๐น) = ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น))
8 distrpr 11023 . . . . . . . . . 10 (๐น ยทP (๐ต +P ๐ถ)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ))
9 mulcompr 11018 . . . . . . . . . 10 ((๐ต +P ๐ถ) ยทP ๐น) = (๐น ยทP (๐ต +P ๐ถ))
10 mulcompr 11018 . . . . . . . . . . 11 (๐ต ยทP ๐น) = (๐น ยทP ๐ต)
11 mulcompr 11018 . . . . . . . . . . 11 (๐ถ ยทP ๐น) = (๐น ยทP ๐ถ)
1210, 11oveq12i 7421 . . . . . . . . . 10 ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) = ((๐น ยทP ๐ต) +P (๐น ยทP ๐ถ))
138, 9, 123eqtr4i 2771 . . . . . . . . 9 ((๐ต +P ๐ถ) ยทP ๐น) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น))
141, 7, 133eqtr3g 2796 . . . . . . . 8 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) = ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)))
1514oveq1d 7424 . . . . . . 7 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)))
16 addasspr 11017 . . . . . . . 8 (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)))
17 oveq2 7417 . . . . . . . . . 10 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (๐ถ ยทP (๐น +P ๐‘†)) = (๐ถ ยทP (๐บ +P ๐‘…)))
18 distrpr 11023 . . . . . . . . . 10 (๐ถ ยทP (๐น +P ๐‘†)) = ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))
19 distrpr 11023 . . . . . . . . . 10 (๐ถ ยทP (๐บ +P ๐‘…)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))
2017, 18, 193eqtr3g 2796 . . . . . . . . 9 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†)) = ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…)))
2120oveq2d 7425 . . . . . . . 8 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐น) +P (๐ถ ยทP ๐‘†))) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
2216, 21eqtrid 2785 . . . . . . 7 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (((๐ต ยทP ๐น) +P (๐ถ ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
2315, 22sylan9eq 2793 . . . . . 6 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))))
24 ovex 7442 . . . . . . 7 (๐ด ยทP ๐น) โˆˆ V
25 ovex 7442 . . . . . . 7 (๐ท ยทP ๐น) โˆˆ V
26 ovex 7442 . . . . . . 7 (๐ถ ยทP ๐‘†) โˆˆ V
27 addcompr 11016 . . . . . . 7 (๐‘ฅ +P ๐‘ฆ) = (๐‘ฆ +P ๐‘ฅ)
28 addasspr 11017 . . . . . . 7 ((๐‘ฅ +P ๐‘ฆ) +P ๐‘ง) = (๐‘ฅ +P (๐‘ฆ +P ๐‘ง))
2924, 25, 26, 27, 28caov32 7634 . . . . . 6 (((๐ด ยทP ๐น) +P (๐ท ยทP ๐น)) +P (๐ถ ยทP ๐‘†)) = (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))
30 ovex 7442 . . . . . . 7 (๐ต ยทP ๐น) โˆˆ V
31 ovex 7442 . . . . . . 7 (๐ถ ยทP ๐บ) โˆˆ V
32 ovex 7442 . . . . . . 7 (๐ถ ยทP ๐‘…) โˆˆ V
3330, 31, 32, 27, 28caov12 7635 . . . . . 6 ((๐ต ยทP ๐น) +P ((๐ถ ยทP ๐บ) +P (๐ถ ยทP ๐‘…))) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))
3423, 29, 333eqtr3g 2796 . . . . 5 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น)) = ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
3534oveq2d 7425 . . . 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 7417 . . . . . . . . . . 11 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ (๐ท ยทP (๐น +P ๐‘†)) = (๐ท ยทP (๐บ +P ๐‘…)))
37 distrpr 11023 . . . . . . . . . . 11 (๐ท ยทP (๐น +P ๐‘†)) = ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))
38 distrpr 11023 . . . . . . . . . . 11 (๐ท ยทP (๐บ +P ๐‘…)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))
3936, 37, 383eqtr3g 2796 . . . . . . . . . 10 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†)) = ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
4039oveq2d 7425 . . . . . . . . 9 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
41 addasspr 11017 . . . . . . . . 9 (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐บ) +P (๐ท ยทP ๐‘…)))
4240, 41eqtr4di 2791 . . . . . . . 8 ((๐น +P ๐‘†) = (๐บ +P ๐‘…) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
43 oveq1 7416 . . . . . . . . . 10 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ต +P ๐ถ) ยทP ๐บ))
44 distrpr 11023 . . . . . . . . . . 11 (๐บ ยทP (๐ด +P ๐ท)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท))
45 mulcompr 11018 . . . . . . . . . . 11 ((๐ด +P ๐ท) ยทP ๐บ) = (๐บ ยทP (๐ด +P ๐ท))
46 mulcompr 11018 . . . . . . . . . . . 12 (๐ด ยทP ๐บ) = (๐บ ยทP ๐ด)
47 mulcompr 11018 . . . . . . . . . . . 12 (๐ท ยทP ๐บ) = (๐บ ยทP ๐ท)
4846, 47oveq12i 7421 . . . . . . . . . . 11 ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) = ((๐บ ยทP ๐ด) +P (๐บ ยทP ๐ท))
4944, 45, 483eqtr4i 2771 . . . . . . . . . 10 ((๐ด +P ๐ท) ยทP ๐บ) = ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ))
50 distrpr 11023 . . . . . . . . . . 11 (๐บ ยทP (๐ต +P ๐ถ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ))
51 mulcompr 11018 . . . . . . . . . . 11 ((๐ต +P ๐ถ) ยทP ๐บ) = (๐บ ยทP (๐ต +P ๐ถ))
52 mulcompr 11018 . . . . . . . . . . . 12 (๐ต ยทP ๐บ) = (๐บ ยทP ๐ต)
53 mulcompr 11018 . . . . . . . . . . . 12 (๐ถ ยทP ๐บ) = (๐บ ยทP ๐ถ)
5452, 53oveq12i 7421 . . . . . . . . . . 11 ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) = ((๐บ ยทP ๐ต) +P (๐บ ยทP ๐ถ))
5550, 51, 543eqtr4i 2771 . . . . . . . . . 10 ((๐ต +P ๐ถ) ยทP ๐บ) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ))
5643, 49, 553eqtr3g 2796 . . . . . . . . 9 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) = ((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)))
5756oveq1d 7424 . . . . . . . 8 ((๐ด +P ๐ท) = (๐ต +P ๐ถ) โ†’ (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
5842, 57sylan9eqr 2795 . . . . . . 7 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)))
59 ovex 7442 . . . . . . . 8 (๐ด ยทP ๐บ) โˆˆ V
60 ovex 7442 . . . . . . . 8 (๐ท ยทP ๐‘†) โˆˆ V
6159, 25, 60, 27, 28caov12 7635 . . . . . . 7 ((๐ด ยทP ๐บ) +P ((๐ท ยทP ๐น) +P (๐ท ยทP ๐‘†))) = ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)))
62 ovex 7442 . . . . . . . 8 (๐ต ยทP ๐บ) โˆˆ V
63 ovex 7442 . . . . . . . 8 (๐ท ยทP ๐‘…) โˆˆ V
6462, 31, 63, 27, 28caov32 7634 . . . . . . 7 (((๐ต ยทP ๐บ) +P (๐ถ ยทP ๐บ)) +P (๐ท ยทP ๐‘…)) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ))
6558, 61, 643eqtr3g 2796 . . . . . 6 (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โˆง (๐น +P ๐‘†) = (๐บ +P ๐‘…)) โ†’ ((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)))
6665oveq1d 7424 . . . . 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 11017 . . . . 5 ((((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (๐ถ ยทP ๐บ)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P ((๐ถ ยทP ๐บ) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
6866, 67eqtrdi 2789 . . . 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 2776 . . 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 7442 . . . 4 ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) โˆˆ V
71 ovex 7442 . . . 4 ((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) โˆˆ V
7270, 71, 25, 27, 28caov13 7637 . . 3 (((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…)) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P (๐ท ยทP ๐น))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…))))
73 addasspr 11017 . . 3 (((๐ท ยทP ๐น) +P ((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†))) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))))
7469, 72, 733eqtr3g 2796 . 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 7638 . . 3 (((๐ด ยทP ๐น) +P (๐ถ ยทP ๐‘†)) +P ((๐ต ยทP ๐บ) +P (๐ท ยทP ๐‘…))) = (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐‘†) +P (๐ท ยทP ๐‘…)))
7675oveq2i 7420 . 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 7640 . . 3 (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…))) = (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†)))
7877oveq2i 7420 . 2 ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ท ยทP ๐‘†)) +P ((๐ต ยทP ๐น) +P (๐ถ ยทP ๐‘…)))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐‘…) +P (๐ท ยทP ๐‘†))))
7974, 76, 783eqtr3g 2796 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 397   = wceq 1542  (class class class)co 7409   +P cpp 10856   ยทP cmp 10857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-omul 8471  df-er 8703  df-ni 10867  df-pli 10868  df-mi 10869  df-lti 10870  df-plpq 10903  df-mpq 10904  df-ltpq 10905  df-enq 10906  df-nq 10907  df-erq 10908  df-plq 10909  df-mq 10910  df-1nq 10911  df-rq 10912  df-ltnq 10913  df-np 10976  df-plp 10978  df-mp 10979
This theorem is referenced by:  mulcmpblnr  11066
  Copyright terms: Public domain W3C validator