Step | Hyp | Ref
| Expression |
1 | | simp23 1209 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) |
2 | | simp3l 1202 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐))) |
3 | | simp3r 1203 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) |
4 | | simprl 770 |
. . . . 5
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ ๐บ โ ๐ต) |
5 | | simprr 772 |
. . . . 5
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ ๐ป โ ๐) |
6 | | simpl2 1193 |
. . . . . 6
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ ๐ธ โ ๐ต) |
7 | | simpl3 1194 |
. . . . . 6
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ ๐น โ ๐ต) |
8 | | simpl1 1192 |
. . . . . . 7
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ ๐) |
9 | | mdetuni.li |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
10 | 8, 9 | syl 17 |
. . . . . 6
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
11 | | reseq1 5935 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ธ โ (๐ฅ โพ ({๐ค} ร ๐)) = (๐ธ โพ ({๐ค} ร ๐))) |
12 | 11 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ ((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โ (๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))))) |
13 | | reseq1 5935 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ธ โ (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ธ โพ ((๐ โ {๐ค}) ร ๐))) |
14 | 13 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ ((๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โ (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)))) |
15 | 13 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ ((๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐)) โ (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐)))) |
16 | 12, 14, 15 | 3anbi123d 1437 |
. . . . . . . . 9
โข (๐ฅ = ๐ธ โ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ ((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))))) |
17 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ (๐ทโ๐ฅ) = (๐ทโ๐ธ)) |
18 | 17 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ฅ = ๐ธ โ ((๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)) โ (๐ทโ๐ธ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) |
19 | 16, 18 | imbi12d 345 |
. . . . . . . 8
โข (๐ฅ = ๐ธ โ ((((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง))) โ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง))))) |
20 | 19 | 2ralbidv 3209 |
. . . . . . 7
โข (๐ฅ = ๐ธ โ (โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง))) โ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง))))) |
21 | | reseq1 5935 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐น โ (๐ฆ โพ ({๐ค} ร ๐)) = (๐น โพ ({๐ค} ร ๐))) |
22 | 21 | oveq1d 7376 |
. . . . . . . . . . 11
โข (๐ฆ = ๐น โ ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐)))) |
23 | 22 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ฆ = ๐น โ ((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โ (๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))))) |
24 | | reseq1 5935 |
. . . . . . . . . . 11
โข (๐ฆ = ๐น โ (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐))) |
25 | 24 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ฆ = ๐น โ ((๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โ (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)))) |
26 | 23, 25 | 3anbi12d 1438 |
. . . . . . . . 9
โข (๐ฆ = ๐น โ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ ((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))))) |
27 | | fveq2 6846 |
. . . . . . . . . . 11
โข (๐ฆ = ๐น โ (๐ทโ๐ฆ) = (๐ทโ๐น)) |
28 | 27 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ฆ = ๐น โ ((๐ทโ๐ฆ) + (๐ทโ๐ง)) = ((๐ทโ๐น) + (๐ทโ๐ง))) |
29 | 28 | eqeq2d 2744 |
. . . . . . . . 9
โข (๐ฆ = ๐น โ ((๐ทโ๐ธ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง)))) |
30 | 26, 29 | imbi12d 345 |
. . . . . . . 8
โข (๐ฆ = ๐น โ ((((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง))) โ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง))))) |
31 | 30 | 2ralbidv 3209 |
. . . . . . 7
โข (๐ฆ = ๐น โ (โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง))) โ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง))))) |
32 | 20, 31 | rspc2va 3593 |
. . . . . 6
โข (((๐ธ โ ๐ต โง ๐น โ ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) โ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง)))) |
33 | 6, 7, 10, 32 | syl21anc 837 |
. . . . 5
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง)))) |
34 | | reseq1 5935 |
. . . . . . . . . 10
โข (๐ง = ๐บ โ (๐ง โพ ({๐ค} ร ๐)) = (๐บ โพ ({๐ค} ร ๐))) |
35 | 34 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ง = ๐บ โ ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐)))) |
36 | 35 | eqeq2d 2744 |
. . . . . . . 8
โข (๐ง = ๐บ โ ((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โ (๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))))) |
37 | | reseq1 5935 |
. . . . . . . . 9
โข (๐ง = ๐บ โ (๐ง โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐))) |
38 | 37 | eqeq2d 2744 |
. . . . . . . 8
โข (๐ง = ๐บ โ ((๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐)) โ (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐)))) |
39 | 36, 38 | 3anbi13d 1439 |
. . . . . . 7
โข (๐ง = ๐บ โ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ ((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐))))) |
40 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ง = ๐บ โ (๐ทโ๐ง) = (๐ทโ๐บ)) |
41 | 40 | oveq2d 7377 |
. . . . . . . 8
โข (๐ง = ๐บ โ ((๐ทโ๐น) + (๐ทโ๐ง)) = ((๐ทโ๐น) + (๐ทโ๐บ))) |
42 | 41 | eqeq2d 2744 |
. . . . . . 7
โข (๐ง = ๐บ โ ((๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง)) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ)))) |
43 | 39, 42 | imbi12d 345 |
. . . . . 6
โข (๐ง = ๐บ โ ((((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง))) โ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ))))) |
44 | | sneq 4600 |
. . . . . . . . . . 11
โข (๐ค = ๐ป โ {๐ค} = {๐ป}) |
45 | 44 | xpeq1d 5666 |
. . . . . . . . . 10
โข (๐ค = ๐ป โ ({๐ค} ร ๐) = ({๐ป} ร ๐)) |
46 | 45 | reseq2d 5941 |
. . . . . . . . 9
โข (๐ค = ๐ป โ (๐ธ โพ ({๐ค} ร ๐)) = (๐ธ โพ ({๐ป} ร ๐))) |
47 | 45 | reseq2d 5941 |
. . . . . . . . . 10
โข (๐ค = ๐ป โ (๐น โพ ({๐ค} ร ๐)) = (๐น โพ ({๐ป} ร ๐))) |
48 | 45 | reseq2d 5941 |
. . . . . . . . . 10
โข (๐ค = ๐ป โ (๐บ โพ ({๐ค} ร ๐)) = (๐บ โพ ({๐ป} ร ๐))) |
49 | 47, 48 | oveq12d 7379 |
. . . . . . . . 9
โข (๐ค = ๐ป โ ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) |
50 | 46, 49 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ค = ๐ป โ ((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))) โ (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))))) |
51 | 44 | difeq2d 4086 |
. . . . . . . . . . 11
โข (๐ค = ๐ป โ (๐ โ {๐ค}) = (๐ โ {๐ป})) |
52 | 51 | xpeq1d 5666 |
. . . . . . . . . 10
โข (๐ค = ๐ป โ ((๐ โ {๐ค}) ร ๐) = ((๐ โ {๐ป}) ร ๐)) |
53 | 52 | reseq2d 5941 |
. . . . . . . . 9
โข (๐ค = ๐ป โ (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ธ โพ ((๐ โ {๐ป}) ร ๐))) |
54 | 52 | reseq2d 5941 |
. . . . . . . . 9
โข (๐ค = ๐ป โ (๐น โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐))) |
55 | 53, 54 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ค = ๐ป โ ((๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โ (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)))) |
56 | 52 | reseq2d 5941 |
. . . . . . . . 9
โข (๐ค = ๐ป โ (๐บ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) |
57 | 53, 56 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ค = ๐ป โ ((๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐)) โ (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) |
58 | 50, 55, 57 | 3anbi123d 1437 |
. . . . . . 7
โข (๐ค = ๐ป โ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐))) โ ((๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))))) |
59 | 58 | imbi1d 342 |
. . . . . 6
โข (๐ค = ๐ป โ ((((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐บ โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐บ โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ))) โ (((๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ))))) |
60 | 43, 59 | rspc2va 3593 |
. . . . 5
โข (((๐บ โ ๐ต โง ๐ป โ ๐) โง โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ธ โพ ({๐ค} ร ๐)) = ((๐น โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐น โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐ง)))) โ (((๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ)))) |
61 | 4, 5, 33, 60 | syl21anc 837 |
. . . 4
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐)) โ (((๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ)))) |
62 | 61 | 3adantr3 1172 |
. . 3
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))))) โ (((๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ)))) |
63 | 62 | 3adant3 1133 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (((๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ)))) |
64 | 1, 2, 3, 63 | mp3and 1465 |
1
โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ))) |