Step | Hyp | Ref
| Expression |
1 | | affinecomb1.a |
. . 3
โข (๐ โ ๐ด โ โ) |
2 | | affinecomb1.b |
. . 3
โข (๐ โ ๐ต โ โ) |
3 | | affinecomb1.c |
. . 3
โข (๐ โ ๐ถ โ โ) |
4 | | affinecomb1.d |
. . 3
โข (๐ โ ๐ต โ ๐ถ) |
5 | | affinecomb1.e |
. . 3
โข (๐ โ ๐ธ โ โ) |
6 | | affinecomb1.f |
. . 3
โข (๐ โ ๐น โ โ) |
7 | | affinecomb1.g |
. . 3
โข (๐ โ ๐บ โ โ) |
8 | | eqid 2733 |
. . 3
โข ((๐บ โ ๐น) / (๐ถ โ ๐ต)) = ((๐บ โ ๐น) / (๐ถ โ ๐ต)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | affinecomb1 46878 |
. 2
โข (๐ โ (โ๐ก โ โ (๐ด = (((1 โ ๐ก) ยท ๐ต) + (๐ก ยท ๐ถ)) โง ๐ธ = (((1 โ ๐ก) ยท ๐น) + (๐ก ยท ๐บ))) โ ๐ธ = ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น))) |
10 | 5 | recnd 11191 |
. . 3
โข (๐ โ ๐ธ โ โ) |
11 | 7 | recnd 11191 |
. . . . . . 7
โข (๐ โ ๐บ โ โ) |
12 | 6 | recnd 11191 |
. . . . . . 7
โข (๐ โ ๐น โ โ) |
13 | 11, 12 | subcld 11520 |
. . . . . 6
โข (๐ โ (๐บ โ ๐น) โ โ) |
14 | 3 | recnd 11191 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
15 | 2 | recnd 11191 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
16 | 14, 15 | subcld 11520 |
. . . . . 6
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
17 | 4 | necomd 2996 |
. . . . . . 7
โข (๐ โ ๐ถ โ ๐ต) |
18 | 14, 15, 17 | subne0d 11529 |
. . . . . 6
โข (๐ โ (๐ถ โ ๐ต) โ 0) |
19 | 13, 16, 18 | divcld 11939 |
. . . . 5
โข (๐ โ ((๐บ โ ๐น) / (๐ถ โ ๐ต)) โ โ) |
20 | 1 | recnd 11191 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
21 | 20, 15 | subcld 11520 |
. . . . 5
โข (๐ โ (๐ด โ ๐ต) โ โ) |
22 | 19, 21 | mulcld 11183 |
. . . 4
โข (๐ โ (((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) โ โ) |
23 | 22, 12 | addcld 11182 |
. . 3
โข (๐ โ ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น) โ โ) |
24 | 10, 23, 16, 18 | mulcand 11796 |
. 2
โข (๐ โ (((๐ถ โ ๐ต) ยท ๐ธ) = ((๐ถ โ ๐ต) ยท ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น)) โ ๐ธ = ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น))) |
25 | 16, 22, 12 | adddid 11187 |
. . . 4
โข (๐ โ ((๐ถ โ ๐ต) ยท ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น)) = (((๐ถ โ ๐ต) ยท (((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต))) + ((๐ถ โ ๐ต) ยท ๐น))) |
26 | 13, 16, 18 | divcan2d 11941 |
. . . . . . . 8
โข (๐ โ ((๐ถ โ ๐ต) ยท ((๐บ โ ๐น) / (๐ถ โ ๐ต))) = (๐บ โ ๐น)) |
27 | 26 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐บ โ ๐น) / (๐ถ โ ๐ต))) ยท (๐ด โ ๐ต)) = ((๐บ โ ๐น) ยท (๐ด โ ๐ต))) |
28 | 16, 19, 21 | mulassd 11186 |
. . . . . . 7
โข (๐ โ (((๐ถ โ ๐ต) ยท ((๐บ โ ๐น) / (๐ถ โ ๐ต))) ยท (๐ด โ ๐ต)) = ((๐ถ โ ๐ต) ยท (((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)))) |
29 | 13, 20, 15 | subdid 11619 |
. . . . . . 7
โข (๐ โ ((๐บ โ ๐น) ยท (๐ด โ ๐ต)) = (((๐บ โ ๐น) ยท ๐ด) โ ((๐บ โ ๐น) ยท ๐ต))) |
30 | 27, 28, 29 | 3eqtr3d 2781 |
. . . . . 6
โข (๐ โ ((๐ถ โ ๐ต) ยท (((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต))) = (((๐บ โ ๐น) ยท ๐ด) โ ((๐บ โ ๐น) ยท ๐ต))) |
31 | 14, 15, 12 | subdird 11620 |
. . . . . 6
โข (๐ โ ((๐ถ โ ๐ต) ยท ๐น) = ((๐ถ ยท ๐น) โ (๐ต ยท ๐น))) |
32 | 30, 31 | oveq12d 7379 |
. . . . 5
โข (๐ โ (((๐ถ โ ๐ต) ยท (((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต))) + ((๐ถ โ ๐ต) ยท ๐น)) = ((((๐บ โ ๐น) ยท ๐ด) โ ((๐บ โ ๐น) ยท ๐ต)) + ((๐ถ ยท ๐น) โ (๐ต ยท ๐น)))) |
33 | 13, 20 | mulcld 11183 |
. . . . . 6
โข (๐ โ ((๐บ โ ๐น) ยท ๐ด) โ โ) |
34 | 13, 15 | mulcld 11183 |
. . . . . 6
โข (๐ โ ((๐บ โ ๐น) ยท ๐ต) โ โ) |
35 | 14, 12 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (๐ถ ยท ๐น) โ โ) |
36 | 15, 12 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (๐ต ยท ๐น) โ โ) |
37 | 35, 36 | subcld 11520 |
. . . . . 6
โข (๐ โ ((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) โ โ) |
38 | 33, 34, 37 | subadd23d 11542 |
. . . . 5
โข (๐ โ ((((๐บ โ ๐น) ยท ๐ด) โ ((๐บ โ ๐น) ยท ๐ต)) + ((๐ถ ยท ๐น) โ (๐ต ยท ๐น))) = (((๐บ โ ๐น) ยท ๐ด) + (((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) โ ((๐บ โ ๐น) ยท ๐ต)))) |
39 | 32, 38 | eqtrd 2773 |
. . . 4
โข (๐ โ (((๐ถ โ ๐ต) ยท (((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต))) + ((๐ถ โ ๐ต) ยท ๐น)) = (((๐บ โ ๐น) ยท ๐ด) + (((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) โ ((๐บ โ ๐น) ยท ๐ต)))) |
40 | 14, 12 | mulcomd 11184 |
. . . . . . . 8
โข (๐ โ (๐ถ ยท ๐น) = (๐น ยท ๐ถ)) |
41 | 15, 12 | mulcomd 11184 |
. . . . . . . 8
โข (๐ โ (๐ต ยท ๐น) = (๐น ยท ๐ต)) |
42 | 40, 41 | oveq12d 7379 |
. . . . . . 7
โข (๐ โ ((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) = ((๐น ยท ๐ถ) โ (๐น ยท ๐ต))) |
43 | 11, 12, 15 | subdird 11620 |
. . . . . . 7
โข (๐ โ ((๐บ โ ๐น) ยท ๐ต) = ((๐บ ยท ๐ต) โ (๐น ยท ๐ต))) |
44 | 42, 43 | oveq12d 7379 |
. . . . . 6
โข (๐ โ (((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) โ ((๐บ โ ๐น) ยท ๐ต)) = (((๐น ยท ๐ถ) โ (๐น ยท ๐ต)) โ ((๐บ ยท ๐ต) โ (๐น ยท ๐ต)))) |
45 | 12, 14 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (๐น ยท ๐ถ) โ โ) |
46 | 11, 15 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (๐บ ยท ๐ต) โ โ) |
47 | 12, 15 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (๐น ยท ๐ต) โ โ) |
48 | 45, 46, 47 | nnncan2d 11555 |
. . . . . 6
โข (๐ โ (((๐น ยท ๐ถ) โ (๐น ยท ๐ต)) โ ((๐บ ยท ๐ต) โ (๐น ยท ๐ต))) = ((๐น ยท ๐ถ) โ (๐บ ยท ๐ต))) |
49 | 11, 15 | mulcomd 11184 |
. . . . . . 7
โข (๐ โ (๐บ ยท ๐ต) = (๐ต ยท ๐บ)) |
50 | 49 | oveq2d 7377 |
. . . . . 6
โข (๐ โ ((๐น ยท ๐ถ) โ (๐บ ยท ๐ต)) = ((๐น ยท ๐ถ) โ (๐ต ยท ๐บ))) |
51 | 44, 48, 50 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ (((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) โ ((๐บ โ ๐น) ยท ๐ต)) = ((๐น ยท ๐ถ) โ (๐ต ยท ๐บ))) |
52 | 51 | oveq2d 7377 |
. . . 4
โข (๐ โ (((๐บ โ ๐น) ยท ๐ด) + (((๐ถ ยท ๐น) โ (๐ต ยท ๐น)) โ ((๐บ โ ๐น) ยท ๐ต))) = (((๐บ โ ๐น) ยท ๐ด) + ((๐น ยท ๐ถ) โ (๐ต ยท ๐บ)))) |
53 | 25, 39, 52 | 3eqtrd 2777 |
. . 3
โข (๐ โ ((๐ถ โ ๐ต) ยท ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น)) = (((๐บ โ ๐น) ยท ๐ด) + ((๐น ยท ๐ถ) โ (๐ต ยท ๐บ)))) |
54 | 53 | eqeq2d 2744 |
. 2
โข (๐ โ (((๐ถ โ ๐ต) ยท ๐ธ) = ((๐ถ โ ๐ต) ยท ((((๐บ โ ๐น) / (๐ถ โ ๐ต)) ยท (๐ด โ ๐ต)) + ๐น)) โ ((๐ถ โ ๐ต) ยท ๐ธ) = (((๐บ โ ๐น) ยท ๐ด) + ((๐น ยท ๐ถ) โ (๐ต ยท ๐บ))))) |
55 | 9, 24, 54 | 3bitr2d 307 |
1
โข (๐ โ (โ๐ก โ โ (๐ด = (((1 โ ๐ก) ยท ๐ต) + (๐ก ยท ๐ถ)) โง ๐ธ = (((1 โ ๐ก) ยท ๐น) + (๐ก ยท ๐บ))) โ ((๐ถ โ ๐ต) ยท ๐ธ) = (((๐บ โ ๐น) ยท ๐ด) + ((๐น ยท ๐ถ) โ (๐ต ยท ๐บ))))) |