Step | Hyp | Ref
| Expression |
1 | | znval.y |
. 2
β’ π =
(β€/nβ€βπ) |
2 | | zringring 20888 |
. . . . 5
β’
β€ring β Ring |
3 | 2 | a1i 11 |
. . . 4
β’ (π = π β β€ring β
Ring) |
4 | | ovexd 7397 |
. . . . 5
β’ ((π = π β§ π§ = β€ring) β (π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) β V) |
5 | | id 22 |
. . . . . . 7
β’ (π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π}))) β π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) |
6 | | simpr 486 |
. . . . . . . . 9
β’ ((π = π β§ π§ = β€ring) β π§ =
β€ring) |
7 | 6 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ ((π = π β§ π§ = β€ring) β
(RSpanβπ§) =
(RSpanββ€ring)) |
8 | | znval.s |
. . . . . . . . . . . 12
β’ π =
(RSpanββ€ring) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ ((π = π β§ π§ = β€ring) β
(RSpanβπ§) = π) |
10 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π = π β§ π§ = β€ring) β π = π) |
11 | 10 | sneqd 4603 |
. . . . . . . . . . 11
β’ ((π = π β§ π§ = β€ring) β {π} = {π}) |
12 | 9, 11 | fveq12d 6854 |
. . . . . . . . . 10
β’ ((π = π β§ π§ = β€ring) β
((RSpanβπ§)β{π}) = (πβ{π})) |
13 | 6, 12 | oveq12d 7380 |
. . . . . . . . 9
β’ ((π = π β§ π§ = β€ring) β (π§ ~QG
((RSpanβπ§)β{π})) = (β€ring
~QG (πβ{π}))) |
14 | 6, 13 | oveq12d 7380 |
. . . . . . . 8
β’ ((π = π β§ π§ = β€ring) β (π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) = (β€ring
/s (β€ring ~QG (πβ{π})))) |
15 | | znval.u |
. . . . . . . 8
β’ π = (β€ring
/s (β€ring ~QG (πβ{π}))) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . 7
β’ ((π = π β§ π§ = β€ring) β (π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) = π) |
17 | 5, 16 | sylan9eqr 2799 |
. . . . . 6
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β π = π) |
18 | | fvex 6860 |
. . . . . . . . . 10
β’
(β€RHomβπ ) β V |
19 | 18 | resex 5990 |
. . . . . . . . 9
β’
((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) β V |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) β V) |
21 | | id 22 |
. . . . . . . . . . . 12
β’ (π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) β π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π)))) |
22 | 17 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β (β€RHomβπ ) = (β€RHomβπ)) |
23 | | simpll 766 |
. . . . . . . . . . . . . . . . 17
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β π = π) |
24 | 23 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β (π = 0 β π = 0)) |
25 | 23 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β (0..^π) = (0..^π)) |
26 | 24, 25 | ifbieq2d 4517 |
. . . . . . . . . . . . . . 15
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β if(π = 0, β€, (0..^π)) = if(π = 0, β€, (0..^π))) |
27 | | znval.w |
. . . . . . . . . . . . . . 15
β’ π = if(π = 0, β€, (0..^π)) |
28 | 26, 27 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β if(π = 0, β€, (0..^π)) = π) |
29 | 22, 28 | reseq12d 5943 |
. . . . . . . . . . . . 13
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) = ((β€RHomβπ) βΎ π)) |
30 | | znval.f |
. . . . . . . . . . . . 13
β’ πΉ = ((β€RHomβπ) βΎ π) |
31 | 29, 30 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) = πΉ) |
32 | 21, 31 | sylan9eqr 2799 |
. . . . . . . . . . 11
β’ ((((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β§ π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π)))) β π = πΉ) |
33 | 32 | coeq1d 5822 |
. . . . . . . . . 10
β’ ((((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β§ π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π)))) β (π β β€ ) = (πΉ β β€ )) |
34 | 32 | cnveqd 5836 |
. . . . . . . . . 10
β’ ((((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β§ π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π)))) β β‘π = β‘πΉ) |
35 | 33, 34 | coeq12d 5825 |
. . . . . . . . 9
β’ ((((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β§ π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π)))) β ((π β β€ ) β β‘π) = ((πΉ β β€ ) β β‘πΉ)) |
36 | | znval.l |
. . . . . . . . 9
β’ β€ = ((πΉ β β€ ) β β‘πΉ) |
37 | 35, 36 | eqtr4di 2795 |
. . . . . . . 8
β’ ((((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β§ π = ((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π)))) β ((π β β€ ) β β‘π) = β€ ) |
38 | 20, 37 | csbied 3898 |
. . . . . . 7
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π) = β€ ) |
39 | 38 | opeq2d 4842 |
. . . . . 6
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β© = β¨(leβndx), β€
β©) |
40 | 17, 39 | oveq12d 7380 |
. . . . 5
β’ (((π = π β§ π§ = β€ring) β§ π = (π§ /s (π§ ~QG ((RSpanβπ§)β{π})))) β (π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©) = (π sSet β¨(leβndx), β€
β©)) |
41 | 4, 40 | csbied 3898 |
. . . 4
β’ ((π = π β§ π§ = β€ring) β
β¦(π§
/s (π§
~QG ((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©) = (π sSet β¨(leβndx), β€
β©)) |
42 | 3, 41 | csbied 3898 |
. . 3
β’ (π = π β
β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©) = (π sSet β¨(leβndx), β€
β©)) |
43 | | df-zn 20923 |
. . 3
β’
β€/nβ€ = (π β β0 β¦
β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG
((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx),
β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©)) |
44 | | ovex 7395 |
. . 3
β’ (π sSet β¨(leβndx),
β€
β©) β V |
45 | 42, 43, 44 | fvmpt 6953 |
. 2
β’ (π β β0
β (β€/nβ€βπ) = (π sSet β¨(leβndx), β€
β©)) |
46 | 1, 45 | eqtrid 2789 |
1
β’ (π β β0
β π = (π sSet β¨(leβndx),
β€
β©)) |