Step | Hyp | Ref
| 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 ๐ท) |
6 | 4, 5 | oveq12i 7421 |
. . . . . . . . . 10
โข ((๐ด
ยทP ๐น) +P (๐ท
ยทP ๐น)) = ((๐น ยทP ๐ด) +P
(๐น
ยทP ๐ท)) |
7 | 2, 3, 6 | 3eqtr4i 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 ๐ถ) |
12 | 10, 11 | oveq12i 7421 |
. . . . . . . . . 10
โข ((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐น)) = ((๐น ยทP ๐ต) +P
(๐น
ยทP ๐ถ)) |
13 | 8, 9, 12 | 3eqtr4i 2771 |
. . . . . . . . 9
โข ((๐ต +P
๐ถ)
ยทP ๐น) = ((๐ต ยทP ๐น) +P
(๐ถ
ยทP ๐น)) |
14 | 1, 7, 13 | 3eqtr3g 2796 |
. . . . . . . 8
โข ((๐ด +P
๐ท) = (๐ต +P ๐ถ) โ ((๐ด ยทP ๐น) +P
(๐ท
ยทP ๐น)) = ((๐ต ยทP ๐น) +P
(๐ถ
ยทP ๐น))) |
15 | 14 | oveq1d 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 ๐
)) |
20 | 17, 18, 19 | 3eqtr3g 2796 |
. . . . . . . . 9
โข ((๐น +P
๐) = (๐บ +P ๐
) โ ((๐ถ ยทP ๐น) +P
(๐ถ
ยทP ๐)) = ((๐ถ ยทP ๐บ) +P
(๐ถ
ยทP ๐
))) |
21 | 20 | oveq2d 7425 |
. . . . . . . 8
โข ((๐น +P
๐) = (๐บ +P ๐
) โ ((๐ต ยทP ๐น) +P
((๐ถ
ยทP ๐น) +P (๐ถ
ยทP ๐))) = ((๐ต ยทP ๐น) +P
((๐ถ
ยทP ๐บ) +P (๐ถ
ยทP ๐
)))) |
22 | 16, 21 | eqtrid 2785 |
. . . . . . 7
โข ((๐น +P
๐) = (๐บ +P ๐
) โ (((๐ต ยทP ๐น) +P
(๐ถ
ยทP ๐น)) +P (๐ถ
ยทP ๐)) = ((๐ต ยทP ๐น) +P
((๐ถ
ยทP ๐บ) +P (๐ถ
ยทP ๐
)))) |
23 | 15, 22 | sylan9eq 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
๐ง)) |
29 | 24, 25, 26, 27, 28 | caov32 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 |
33 | 30, 31, 32, 27, 28 | caov12 7635 |
. . . . . 6
โข ((๐ต
ยทP ๐น) +P ((๐ถ
ยทP ๐บ) +P (๐ถ
ยทP ๐
))) = ((๐ถ ยทP ๐บ) +P
((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
))) |
34 | 23, 29, 33 | 3eqtr3g 2796 |
. . . . 5
โข (((๐ด +P
๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ (((๐ด ยทP ๐น) +P
(๐ถ
ยทP ๐)) +P (๐ท
ยทP ๐น)) = ((๐ถ ยทP ๐บ) +P
((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
)))) |
35 | 34 | oveq2d 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 ๐
)) |
39 | 36, 37, 38 | 3eqtr3g 2796 |
. . . . . . . . . 10
โข ((๐น +P
๐) = (๐บ +P ๐
) โ ((๐ท ยทP ๐น) +P
(๐ท
ยทP ๐)) = ((๐ท ยทP ๐บ) +P
(๐ท
ยทP ๐
))) |
40 | 39 | oveq2d 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 ๐
))) |
42 | 40, 41 | eqtr4di 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 ๐ท) |
48 | 46, 47 | oveq12i 7421 |
. . . . . . . . . . 11
โข ((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐บ)) = ((๐บ ยทP ๐ด) +P
(๐บ
ยทP ๐ท)) |
49 | 44, 45, 48 | 3eqtr4i 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 ๐ถ) |
54 | 52, 53 | oveq12i 7421 |
. . . . . . . . . . 11
โข ((๐ต
ยทP ๐บ) +P (๐ถ
ยทP ๐บ)) = ((๐บ ยทP ๐ต) +P
(๐บ
ยทP ๐ถ)) |
55 | 50, 51, 54 | 3eqtr4i 2771 |
. . . . . . . . . 10
โข ((๐ต +P
๐ถ)
ยทP ๐บ) = ((๐ต ยทP ๐บ) +P
(๐ถ
ยทP ๐บ)) |
56 | 43, 49, 55 | 3eqtr3g 2796 |
. . . . . . . . 9
โข ((๐ด +P
๐ท) = (๐ต +P ๐ถ) โ ((๐ด ยทP ๐บ) +P
(๐ท
ยทP ๐บ)) = ((๐ต ยทP ๐บ) +P
(๐ถ
ยทP ๐บ))) |
57 | 56 | oveq1d 7424 |
. . . . . . . 8
โข ((๐ด +P
๐ท) = (๐ต +P ๐ถ) โ (((๐ด ยทP ๐บ) +P
(๐ท
ยทP ๐บ)) +P (๐ท
ยทP ๐
)) = (((๐ต ยทP ๐บ) +P
(๐ถ
ยทP ๐บ)) +P (๐ท
ยทP ๐
))) |
58 | 42, 57 | sylan9eqr 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 |
61 | 59, 25, 60, 27, 28 | caov12 7635 |
. . . . . . 7
โข ((๐ด
ยทP ๐บ) +P ((๐ท
ยทP ๐น) +P (๐ท
ยทP ๐))) = ((๐ท ยทP ๐น) +P
((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐))) |
62 | | ovex 7442 |
. . . . . . . 8
โข (๐ต
ยทP ๐บ) โ V |
63 | | ovex 7442 |
. . . . . . . 8
โข (๐ท
ยทP ๐
) โ V |
64 | 62, 31, 63, 27, 28 | caov32 7634 |
. . . . . . 7
โข (((๐ต
ยทP ๐บ) +P (๐ถ
ยทP ๐บ)) +P (๐ท
ยทP ๐
)) = (((๐ต ยทP ๐บ) +P
(๐ท
ยทP ๐
)) +P (๐ถ
ยทP ๐บ)) |
65 | 58, 61, 64 | 3eqtr3g 2796 |
. . . . . 6
โข (((๐ด +P
๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ ((๐ท ยทP ๐น) +P
((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐))) = (((๐ต ยทP ๐บ) +P
(๐ท
ยทP ๐
)) +P (๐ถ
ยทP ๐บ))) |
66 | 65 | oveq1d 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 ๐
)))) |
68 | 66, 67 | eqtrdi 2789 |
. . . 4
โข (((๐ด +P
๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ (((๐ท ยทP ๐น) +P
((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐))) +P ((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
))) = (((๐ต ยทP ๐บ) +P
(๐ท
ยทP ๐
)) +P ((๐ถ
ยทP ๐บ) +P ((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
))))) |
69 | 35, 68 | eqtr4d 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 |
72 | 70, 71, 25, 27, 28 | caov13 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 ๐
)))) |
74 | 69, 72, 73 | 3eqtr3g 2796 |
. 2
โข (((๐ด +P
๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐น) +P (๐ถ
ยทP ๐)) +P ((๐ต
ยทP ๐บ) +P (๐ท
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐)) +P ((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
))))) |
75 | 24, 26, 62, 27, 28, 63 | caov4 7638 |
. . 3
โข (((๐ด
ยทP ๐น) +P (๐ถ
ยทP ๐)) +P ((๐ต
ยทP ๐บ) +P (๐ท
ยทP ๐
))) = (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) |
76 | 75 | oveq2i 7420 |
. 2
โข ((๐ท
ยทP ๐น) +P (((๐ด
ยทP ๐น) +P (๐ถ
ยทP ๐)) +P ((๐ต
ยทP ๐บ) +P (๐ท
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)))) |
77 | 59, 60, 30, 27, 28, 32 | caov42 7640 |
. . 3
โข (((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐)) +P ((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
))) = (((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))) |
78 | 77 | oveq2i 7420 |
. 2
โข ((๐ท
ยทP ๐น) +P (((๐ด
ยทP ๐บ) +P (๐ท
ยทP ๐)) +P ((๐ต
ยทP ๐น) +P (๐ถ
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)))) |
79 | 74, 76, 78 | 3eqtr3g 2796 |
1
โข (((๐ด +P
๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |