Step | Hyp | Ref
| Expression |
1 | | nfcv 2905 |
. . . . 5
โข
โฒ๐ฆ(๐ด ยท ๐ถ) |
2 | | nfcsb1v 3878 |
. . . . . 6
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ด |
3 | | nfcv 2905 |
. . . . . 6
โข
โฒ๐ฅ
ยท |
4 | | nfcsb1v 3878 |
. . . . . 6
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ถ |
5 | 2, 3, 4 | nfov 7383 |
. . . . 5
โข
โฒ๐ฅ(โฆ๐ฆ / ๐ฅโฆ๐ด ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) |
6 | | csbeq1a 3867 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ๐ด = โฆ๐ฆ / ๐ฅโฆ๐ด) |
7 | | csbeq1a 3867 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ๐ถ = โฆ๐ฆ / ๐ฅโฆ๐ถ) |
8 | 6, 7 | oveq12d 7371 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด ยท ๐ถ) = (โฆ๐ฆ / ๐ฅโฆ๐ด ยท โฆ๐ฆ / ๐ฅโฆ๐ถ)) |
9 | 1, 5, 8 | cbvmpt 5214 |
. . . 4
โข (๐ฅ โ ๐ โฆ (๐ด ยท ๐ถ)) = (๐ฆ โ ๐ โฆ (โฆ๐ฆ / ๐ฅโฆ๐ด ยท โฆ๐ฆ / ๐ฅโฆ๐ถ)) |
10 | 9 | oveq2i 7364 |
. . 3
โข (๐ D (๐ฅ โ ๐ โฆ (๐ด ยท ๐ถ))) = (๐ D (๐ฆ โ ๐ โฆ (โฆ๐ฆ / ๐ฅโฆ๐ด ยท โฆ๐ฆ / ๐ฅโฆ๐ถ))) |
11 | 10 | a1i 11 |
. 2
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (๐ด ยท ๐ถ))) = (๐ D (๐ฆ โ ๐ โฆ (โฆ๐ฆ / ๐ฅโฆ๐ด ยท โฆ๐ฆ / ๐ฅโฆ๐ถ)))) |
12 | | dvmptmulf.s |
. . 3
โข (๐ โ ๐ โ {โ, โ}) |
13 | | dvmptmulf.ph |
. . . . . 6
โข
โฒ๐ฅ๐ |
14 | | nfv 1917 |
. . . . . 6
โข
โฒ๐ฅ ๐ฆ โ ๐ |
15 | 13, 14 | nfan 1902 |
. . . . 5
โข
โฒ๐ฅ(๐ โง ๐ฆ โ ๐) |
16 | 2 | nfel1 2921 |
. . . . 5
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ด โ โ |
17 | 15, 16 | nfim 1899 |
. . . 4
โข
โฒ๐ฅ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ด โ โ) |
18 | | eleq1w 2820 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ฅ โ ๐ โ ๐ฆ โ ๐)) |
19 | 18 | anbi2d 629 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((๐ โง ๐ฅ โ ๐) โ (๐ โง ๐ฆ โ ๐))) |
20 | 6 | eleq1d 2822 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด โ โ โ โฆ๐ฆ / ๐ฅโฆ๐ด โ โ)) |
21 | 19, 20 | imbi12d 344 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) โ ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ด โ โ))) |
22 | | dvmptmulf.a |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) |
23 | 17, 21, 22 | chvarfv 2233 |
. . 3
โข ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ด โ โ) |
24 | | nfcv 2905 |
. . . . . . 7
โข
โฒ๐ฅ๐ฆ |
25 | 24 | nfcsb1 3877 |
. . . . . 6
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ต |
26 | | nfcv 2905 |
. . . . . 6
โข
โฒ๐ฅ๐ |
27 | 25, 26 | nfel 2919 |
. . . . 5
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ต โ ๐ |
28 | 15, 27 | nfim 1899 |
. . . 4
โข
โฒ๐ฅ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ต โ ๐) |
29 | | csbeq1a 3867 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต) |
30 | 29 | eleq1d 2822 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ต โ ๐ โ โฆ๐ฆ / ๐ฅโฆ๐ต โ ๐)) |
31 | 19, 30 | imbi12d 344 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) โ ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ต โ ๐))) |
32 | | dvmptmulf.b |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) |
33 | 28, 31, 32 | chvarfv 2233 |
. . 3
โข ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ต โ ๐) |
34 | | nfcv 2905 |
. . . . . . 7
โข
โฒ๐ฆ๐ด |
35 | | csbeq1a 3867 |
. . . . . . . 8
โข (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ด = โฆ๐ฅ / ๐ฆโฆโฆ๐ฆ / ๐ฅโฆ๐ด) |
36 | | csbcow 3868 |
. . . . . . . . . 10
โข
โฆ๐ฅ /
๐ฆโฆโฆ๐ฆ / ๐ฅโฆ๐ด = โฆ๐ฅ / ๐ฅโฆ๐ด |
37 | | csbid 3866 |
. . . . . . . . . 10
โข
โฆ๐ฅ /
๐ฅโฆ๐ด = ๐ด |
38 | 36, 37 | eqtri 2764 |
. . . . . . . . 9
โข
โฆ๐ฅ /
๐ฆโฆโฆ๐ฆ / ๐ฅโฆ๐ด = ๐ด |
39 | 38 | a1i 11 |
. . . . . . . 8
โข (๐ฆ = ๐ฅ โ โฆ๐ฅ / ๐ฆโฆโฆ๐ฆ / ๐ฅโฆ๐ด = ๐ด) |
40 | 35, 39 | eqtrd 2776 |
. . . . . . 7
โข (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ด = ๐ด) |
41 | 2, 34, 40 | cbvmpt 5214 |
. . . . . 6
โข (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ด) = (๐ฅ โ ๐ โฆ ๐ด) |
42 | 41 | oveq2i 7364 |
. . . . 5
โข (๐ D (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ด)) = (๐ D (๐ฅ โ ๐ โฆ ๐ด)) |
43 | 42 | a1i 11 |
. . . 4
โข (๐ โ (๐ D (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ด)) = (๐ D (๐ฅ โ ๐ โฆ ๐ด))) |
44 | | dvmptmulf.ab |
. . . 4
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ ๐ด)) = (๐ฅ โ ๐ โฆ ๐ต)) |
45 | | nfcv 2905 |
. . . . . 6
โข
โฒ๐ฆ๐ต |
46 | 45, 25, 29 | cbvmpt 5214 |
. . . . 5
โข (๐ฅ โ ๐ โฆ ๐ต) = (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ต) |
47 | 46 | a1i 11 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ โฆ ๐ต) = (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ต)) |
48 | 43, 44, 47 | 3eqtrd 2780 |
. . 3
โข (๐ โ (๐ D (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ด)) = (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ต)) |
49 | 4 | nfel1 2921 |
. . . . 5
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ถ โ โ |
50 | 15, 49 | nfim 1899 |
. . . 4
โข
โฒ๐ฅ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ถ โ โ) |
51 | 7 | eleq1d 2822 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ถ โ โ โ โฆ๐ฆ / ๐ฅโฆ๐ถ โ โ)) |
52 | 19, 51 | imbi12d 344 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((๐ โง ๐ฅ โ ๐) โ ๐ถ โ โ) โ ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ถ โ โ))) |
53 | | dvmptmulf.c |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ โ) |
54 | 50, 52, 53 | chvarfv 2233 |
. . 3
โข ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ถ โ โ) |
55 | 24 | nfcsb1 3877 |
. . . . . 6
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ท |
56 | | nfcv 2905 |
. . . . . 6
โข
โฒ๐ฅ๐ |
57 | 55, 56 | nfel 2919 |
. . . . 5
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ท โ ๐ |
58 | 15, 57 | nfim 1899 |
. . . 4
โข
โฒ๐ฅ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ท โ ๐) |
59 | | csbeq1a 3867 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ๐ท = โฆ๐ฆ / ๐ฅโฆ๐ท) |
60 | 59 | eleq1d 2822 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ท โ ๐ โ โฆ๐ฆ / ๐ฅโฆ๐ท โ ๐)) |
61 | 19, 60 | imbi12d 344 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((๐ โง ๐ฅ โ ๐) โ ๐ท โ ๐) โ ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ท โ ๐))) |
62 | | dvmptmulf.d |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ๐ท โ ๐) |
63 | 58, 61, 62 | chvarfv 2233 |
. . 3
โข ((๐ โง ๐ฆ โ ๐) โ โฆ๐ฆ / ๐ฅโฆ๐ท โ ๐) |
64 | | nfcv 2905 |
. . . . . . 7
โข
โฒ๐ฆ๐ถ |
65 | | eqcom 2743 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ ๐ฆ = ๐ฅ) |
66 | 65 | imbi1i 349 |
. . . . . . . . 9
โข ((๐ฅ = ๐ฆ โ ๐ถ = โฆ๐ฆ / ๐ฅโฆ๐ถ) โ (๐ฆ = ๐ฅ โ ๐ถ = โฆ๐ฆ / ๐ฅโฆ๐ถ)) |
67 | | eqcom 2743 |
. . . . . . . . . 10
โข (๐ถ = โฆ๐ฆ / ๐ฅโฆ๐ถ โ โฆ๐ฆ / ๐ฅโฆ๐ถ = ๐ถ) |
68 | 67 | imbi2i 335 |
. . . . . . . . 9
โข ((๐ฆ = ๐ฅ โ ๐ถ = โฆ๐ฆ / ๐ฅโฆ๐ถ) โ (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ถ = ๐ถ)) |
69 | 66, 68 | bitri 274 |
. . . . . . . 8
โข ((๐ฅ = ๐ฆ โ ๐ถ = โฆ๐ฆ / ๐ฅโฆ๐ถ) โ (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ถ = ๐ถ)) |
70 | 7, 69 | mpbi 229 |
. . . . . . 7
โข (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ถ = ๐ถ) |
71 | 4, 64, 70 | cbvmpt 5214 |
. . . . . 6
โข (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ถ) = (๐ฅ โ ๐ โฆ ๐ถ) |
72 | 71 | oveq2i 7364 |
. . . . 5
โข (๐ D (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ถ)) = (๐ D (๐ฅ โ ๐ โฆ ๐ถ)) |
73 | 72 | a1i 11 |
. . . 4
โข (๐ โ (๐ D (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ถ)) = (๐ D (๐ฅ โ ๐ โฆ ๐ถ))) |
74 | | dvmptmulf.cd |
. . . 4
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ ๐ถ)) = (๐ฅ โ ๐ โฆ ๐ท)) |
75 | | nfcv 2905 |
. . . . . 6
โข
โฒ๐ฆ๐ท |
76 | 75, 55, 59 | cbvmpt 5214 |
. . . . 5
โข (๐ฅ โ ๐ โฆ ๐ท) = (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ท) |
77 | 76 | a1i 11 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ โฆ ๐ท) = (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ท)) |
78 | 73, 74, 77 | 3eqtrd 2780 |
. . 3
โข (๐ โ (๐ D (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ถ)) = (๐ฆ โ ๐ โฆ โฆ๐ฆ / ๐ฅโฆ๐ท)) |
79 | 12, 23, 33, 48, 54, 63, 78 | dvmptmul 25309 |
. 2
โข (๐ โ (๐ D (๐ฆ โ ๐ โฆ (โฆ๐ฆ / ๐ฅโฆ๐ด ยท โฆ๐ฆ / ๐ฅโฆ๐ถ))) = (๐ฆ โ ๐ โฆ ((โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) + (โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด)))) |
80 | 25, 3, 4 | nfov 7383 |
. . . . 5
โข
โฒ๐ฅ(โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) |
81 | | nfcv 2905 |
. . . . 5
โข
โฒ๐ฅ
+ |
82 | 55, 3, 2 | nfov 7383 |
. . . . 5
โข
โฒ๐ฅ(โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด) |
83 | 80, 81, 82 | nfov 7383 |
. . . 4
โข
โฒ๐ฅ((โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) + (โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด)) |
84 | | nfcv 2905 |
. . . 4
โข
โฒ๐ฆ((๐ต ยท ๐ถ) + (๐ท ยท ๐ด)) |
85 | 65 | imbi1i 349 |
. . . . . . . 8
โข ((๐ฅ = ๐ฆ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต) โ (๐ฆ = ๐ฅ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต)) |
86 | | eqcom 2743 |
. . . . . . . . 9
โข (๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต โ โฆ๐ฆ / ๐ฅโฆ๐ต = ๐ต) |
87 | 86 | imbi2i 335 |
. . . . . . . 8
โข ((๐ฆ = ๐ฅ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต) โ (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ต = ๐ต)) |
88 | 85, 87 | bitri 274 |
. . . . . . 7
โข ((๐ฅ = ๐ฆ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต) โ (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ต = ๐ต)) |
89 | 29, 88 | mpbi 229 |
. . . . . 6
โข (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ต = ๐ต) |
90 | 89, 70 | oveq12d 7371 |
. . . . 5
โข (๐ฆ = ๐ฅ โ (โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) = (๐ต ยท ๐ถ)) |
91 | 65 | imbi1i 349 |
. . . . . . . 8
โข ((๐ฅ = ๐ฆ โ ๐ท = โฆ๐ฆ / ๐ฅโฆ๐ท) โ (๐ฆ = ๐ฅ โ ๐ท = โฆ๐ฆ / ๐ฅโฆ๐ท)) |
92 | | eqcom 2743 |
. . . . . . . . 9
โข (๐ท = โฆ๐ฆ / ๐ฅโฆ๐ท โ โฆ๐ฆ / ๐ฅโฆ๐ท = ๐ท) |
93 | 92 | imbi2i 335 |
. . . . . . . 8
โข ((๐ฆ = ๐ฅ โ ๐ท = โฆ๐ฆ / ๐ฅโฆ๐ท) โ (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ท = ๐ท)) |
94 | 91, 93 | bitri 274 |
. . . . . . 7
โข ((๐ฅ = ๐ฆ โ ๐ท = โฆ๐ฆ / ๐ฅโฆ๐ท) โ (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ท = ๐ท)) |
95 | 59, 94 | mpbi 229 |
. . . . . 6
โข (๐ฆ = ๐ฅ โ โฆ๐ฆ / ๐ฅโฆ๐ท = ๐ท) |
96 | 95, 40 | oveq12d 7371 |
. . . . 5
โข (๐ฆ = ๐ฅ โ (โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด) = (๐ท ยท ๐ด)) |
97 | 90, 96 | oveq12d 7371 |
. . . 4
โข (๐ฆ = ๐ฅ โ ((โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) + (โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด)) = ((๐ต ยท ๐ถ) + (๐ท ยท ๐ด))) |
98 | 83, 84, 97 | cbvmpt 5214 |
. . 3
โข (๐ฆ โ ๐ โฆ ((โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) + (โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด))) = (๐ฅ โ ๐ โฆ ((๐ต ยท ๐ถ) + (๐ท ยท ๐ด))) |
99 | 98 | a1i 11 |
. 2
โข (๐ โ (๐ฆ โ ๐ โฆ ((โฆ๐ฆ / ๐ฅโฆ๐ต ยท โฆ๐ฆ / ๐ฅโฆ๐ถ) + (โฆ๐ฆ / ๐ฅโฆ๐ท ยท โฆ๐ฆ / ๐ฅโฆ๐ด))) = (๐ฅ โ ๐ โฆ ((๐ต ยท ๐ถ) + (๐ท ยท ๐ด)))) |
100 | 11, 79, 99 | 3eqtrd 2780 |
1
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (๐ด ยท ๐ถ))) = (๐ฅ โ ๐ โฆ ((๐ต ยท ๐ถ) + (๐ท ยท ๐ด)))) |