Step | Hyp | Ref
| Expression |
1 | | dprdff.w |
. . . . 5
β’ π = {β β Xπ β πΌ (πβπ) β£ β finSupp 0 } |
2 | | dprdff.1 |
. . . . 5
β’ (π β πΊdom DProd π) |
3 | | dprdff.2 |
. . . . 5
β’ (π β dom π = πΌ) |
4 | | dprdff.3 |
. . . . 5
β’ (π β πΉ β π) |
5 | | eqid 2737 |
. . . . 5
β’
(BaseβπΊ) =
(BaseβπΊ) |
6 | 1, 2, 3, 4, 5 | dprdff 19798 |
. . . 4
β’ (π β πΉ:πΌβΆ(BaseβπΊ)) |
7 | 6 | ffnd 6674 |
. . 3
β’ (π β πΉ Fn πΌ) |
8 | 6 | ffvelcdmda 7040 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β (πΉβπ¦) β (BaseβπΊ)) |
9 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ = π§) β π¦ = π§) |
10 | 9 | fveq2d 6851 |
. . . . . . . . 9
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ = π§) β (πΉβπ¦) = (πΉβπ§)) |
11 | 9 | equcomd 2023 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ = π§) β π§ = π¦) |
12 | 11 | fveq2d 6851 |
. . . . . . . . 9
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ = π§) β (πΉβπ§) = (πΉβπ¦)) |
13 | 10, 12 | oveq12d 7380 |
. . . . . . . 8
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ = π§) β ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦))) |
14 | 2 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β πΊdom DProd π) |
15 | 3 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β dom π = πΌ) |
16 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β π¦ β πΌ) |
17 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β π§ β πΌ) |
18 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β π¦ β π§) |
19 | | dprdfcntz.z |
. . . . . . . . . . 11
β’ π = (CntzβπΊ) |
20 | 14, 15, 16, 17, 18, 19 | dprdcntz 19794 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β (πβπ¦) β (πβ(πβπ§))) |
21 | 1, 2, 3, 4 | dprdfcl 19799 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΌ) β (πΉβπ¦) β (πβπ¦)) |
22 | 21 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β (πΉβπ¦) β (πβπ¦)) |
23 | 20, 22 | sseldd 3950 |
. . . . . . . . 9
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β (πΉβπ¦) β (πβ(πβπ§))) |
24 | 1, 2, 3, 4 | dprdfcl 19799 |
. . . . . . . . . 10
β’ ((π β§ π§ β πΌ) β (πΉβπ§) β (πβπ§)) |
25 | 24 | ad4ant13 750 |
. . . . . . . . 9
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β (πΉβπ§) β (πβπ§)) |
26 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
27 | 26, 19 | cntzi 19116 |
. . . . . . . . 9
β’ (((πΉβπ¦) β (πβ(πβπ§)) β§ (πΉβπ§) β (πβπ§)) β ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦))) |
28 | 23, 25, 27 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π¦ β πΌ) β§ π§ β πΌ) β§ π¦ β π§) β ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦))) |
29 | 13, 28 | pm2.61dane 3033 |
. . . . . . 7
β’ (((π β§ π¦ β πΌ) β§ π§ β πΌ) β ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦))) |
30 | 29 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β βπ§ β πΌ ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦))) |
31 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β πΉ Fn πΌ) |
32 | | oveq2 7370 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ§) β ((πΉβπ¦)(+gβπΊ)π₯) = ((πΉβπ¦)(+gβπΊ)(πΉβπ§))) |
33 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ§) β (π₯(+gβπΊ)(πΉβπ¦)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦))) |
34 | 32, 33 | eqeq12d 2753 |
. . . . . . . 8
β’ (π₯ = (πΉβπ§) β (((πΉβπ¦)(+gβπΊ)π₯) = (π₯(+gβπΊ)(πΉβπ¦)) β ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦)))) |
35 | 34 | ralrn 7043 |
. . . . . . 7
β’ (πΉ Fn πΌ β (βπ₯ β ran πΉ((πΉβπ¦)(+gβπΊ)π₯) = (π₯(+gβπΊ)(πΉβπ¦)) β βπ§ β πΌ ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦)))) |
36 | 31, 35 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β (βπ₯ β ran πΉ((πΉβπ¦)(+gβπΊ)π₯) = (π₯(+gβπΊ)(πΉβπ¦)) β βπ§ β πΌ ((πΉβπ¦)(+gβπΊ)(πΉβπ§)) = ((πΉβπ§)(+gβπΊ)(πΉβπ¦)))) |
37 | 30, 36 | mpbird 257 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β βπ₯ β ran πΉ((πΉβπ¦)(+gβπΊ)π₯) = (π₯(+gβπΊ)(πΉβπ¦))) |
38 | 6 | frnd 6681 |
. . . . . . 7
β’ (π β ran πΉ β (BaseβπΊ)) |
39 | 38 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β ran πΉ β (BaseβπΊ)) |
40 | 5, 26, 19 | elcntz 19109 |
. . . . . 6
β’ (ran
πΉ β (BaseβπΊ) β ((πΉβπ¦) β (πβran πΉ) β ((πΉβπ¦) β (BaseβπΊ) β§ βπ₯ β ran πΉ((πΉβπ¦)(+gβπΊ)π₯) = (π₯(+gβπΊ)(πΉβπ¦))))) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β ((πΉβπ¦) β (πβran πΉ) β ((πΉβπ¦) β (BaseβπΊ) β§ βπ₯ β ran πΉ((πΉβπ¦)(+gβπΊ)π₯) = (π₯(+gβπΊ)(πΉβπ¦))))) |
42 | 8, 37, 41 | mpbir2and 712 |
. . . 4
β’ ((π β§ π¦ β πΌ) β (πΉβπ¦) β (πβran πΉ)) |
43 | 42 | ralrimiva 3144 |
. . 3
β’ (π β βπ¦ β πΌ (πΉβπ¦) β (πβran πΉ)) |
44 | | ffnfv 7071 |
. . 3
β’ (πΉ:πΌβΆ(πβran πΉ) β (πΉ Fn πΌ β§ βπ¦ β πΌ (πΉβπ¦) β (πβran πΉ))) |
45 | 7, 43, 44 | sylanbrc 584 |
. 2
β’ (π β πΉ:πΌβΆ(πβran πΉ)) |
46 | 45 | frnd 6681 |
1
β’ (π β ran πΉ β (πβran πΉ)) |