Step | Hyp | Ref
| Expression |
1 | | ovex 7395 |
. . . 4
โข
((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ V |
2 | | eqid 2737 |
. . . 4
โข (๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) = (๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
3 | 1, 2 | fnmpti 6649 |
. . 3
โข (๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) Fn (โ0 ร
โค) |
4 | 3 | a1i 11 |
. 2
โข (๐ด โ
(โคโฅโ2) โ (๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) Fn (โ0 ร
โค)) |
5 | 2 | rnmpt 5915 |
. . 3
โข ran
(๐ โ
(โ0 ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) = {๐ โฃ โ๐ โ (โ0 ร
โค)๐ =
((1st โ๐)
+ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))} |
6 | | vex 3452 |
. . . . . . . . . 10
โข ๐ โ V |
7 | | vex 3452 |
. . . . . . . . . 10
โข ๐ โ V |
8 | 6, 7 | op1std 7936 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐โฉ โ (1st โ๐) = ๐) |
9 | 6, 7 | op2ndd 7937 |
. . . . . . . . . 10
โข (๐ = โจ๐, ๐โฉ โ (2nd โ๐) = ๐) |
10 | 9 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐โฉ โ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))
= ((โโ((๐ดโ2) โ 1)) ยท ๐)) |
11 | 8, 10 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = โจ๐, ๐โฉ โ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= (๐ +
((โโ((๐ดโ2)
โ 1)) ยท ๐))) |
12 | 11 | eqeq2d 2748 |
. . . . . . 7
โข (๐ = โจ๐, ๐โฉ โ (๐ = ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท
๐)))) |
13 | 12 | rexxp 5803 |
. . . . . 6
โข
(โ๐ โ
(โ0 ร โค)๐ = ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ โ๐ โ
โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐))) |
14 | 13 | bicomi 223 |
. . . . 5
โข
(โ๐ โ
โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐)) โ โ๐ โ (โ0
ร โค)๐ =
((1st โ๐)
+ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
15 | 14 | a1i 11 |
. . . 4
โข (๐ด โ
(โคโฅโ2) โ (โ๐ โ โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐)) โ โ๐ โ (โ0
ร โค)๐ =
((1st โ๐)
+ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))) |
16 | 15 | abbidv 2806 |
. . 3
โข (๐ด โ
(โคโฅโ2) โ {๐ โฃ โ๐ โ โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐))} = {๐ โฃ โ๐ โ (โ0 ร
โค)๐ =
((1st โ๐)
+ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))}) |
17 | 5, 16 | eqtr4id 2796 |
. 2
โข (๐ด โ
(โคโฅโ2) โ ran (๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) = {๐ โฃ โ๐ โ โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐))}) |
18 | | fveq2 6847 |
. . . . . . . 8
โข (๐ = ๐ โ (1st โ๐) = (1st โ๐)) |
19 | | fveq2 6847 |
. . . . . . . . 9
โข (๐ = ๐ โ (2nd โ๐) = (2nd โ๐)) |
20 | 19 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))
= ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))) |
21 | 18, 20 | oveq12d 7380 |
. . . . . . 7
โข (๐ = ๐ โ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
22 | | ovex 7395 |
. . . . . . 7
โข
((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ V |
23 | 21, 2, 22 | fvmpt 6953 |
. . . . . 6
โข (๐ โ (โ0
ร โค) โ ((๐
โ (โ0 ร โค) โฆ ((1st
โ๐) +
((โโ((๐ดโ2)
โ 1)) ยท (2nd โ๐))))โ๐) = ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
24 | 23 | ad2antrl 727 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) = ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
25 | | fveq2 6847 |
. . . . . . . 8
โข (๐ = ๐ โ (1st โ๐) = (1st โ๐)) |
26 | | fveq2 6847 |
. . . . . . . . 9
โข (๐ = ๐ โ (2nd โ๐) = (2nd โ๐)) |
27 | 26 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))
= ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))) |
28 | 25, 27 | oveq12d 7380 |
. . . . . . 7
โข (๐ = ๐ โ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
29 | | ovex 7395 |
. . . . . . 7
โข
((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ V |
30 | 28, 2, 29 | fvmpt 6953 |
. . . . . 6
โข (๐ โ (โ0
ร โค) โ ((๐
โ (โ0 ร โค) โฆ ((1st
โ๐) +
((โโ((๐ดโ2)
โ 1)) ยท (2nd โ๐))))โ๐) = ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
31 | 30 | ad2antll 728 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) = ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
32 | 24, 31 | eqeq12d 2753 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) = ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) โ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))) |
33 | | rmspecsqrtnq 41258 |
. . . . . . . 8
โข (๐ด โ
(โคโฅโ2) โ (โโ((๐ดโ2) โ 1)) โ (โ โ
โ)) |
34 | 33 | adantr 482 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (โโ((๐ดโ2) โ 1)) โ
(โ โ โ)) |
35 | | nn0ssq 12889 |
. . . . . . . 8
โข
โ0 โ โ |
36 | | xp1st 7958 |
. . . . . . . . 9
โข (๐ โ (โ0
ร โค) โ (1st โ๐) โ
โ0) |
37 | 36 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (1st โ๐) โ
โ0) |
38 | 35, 37 | sselid 3947 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (1st โ๐) โ
โ) |
39 | | xp2nd 7959 |
. . . . . . . . 9
โข (๐ โ (โ0
ร โค) โ (2nd โ๐) โ โค) |
40 | 39 | ad2antrl 727 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (2nd โ๐) โ
โค) |
41 | | zq 12886 |
. . . . . . . 8
โข
((2nd โ๐) โ โค โ (2nd
โ๐) โ
โ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (2nd โ๐) โ
โ) |
43 | | xp1st 7958 |
. . . . . . . . 9
โข (๐ โ (โ0
ร โค) โ (1st โ๐) โ
โ0) |
44 | 43 | ad2antll 728 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (1st โ๐) โ
โ0) |
45 | 35, 44 | sselid 3947 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (1st โ๐) โ
โ) |
46 | | xp2nd 7959 |
. . . . . . . . 9
โข (๐ โ (โ0
ร โค) โ (2nd โ๐) โ โค) |
47 | 46 | ad2antll 728 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (2nd โ๐) โ
โค) |
48 | | zq 12886 |
. . . . . . . 8
โข
((2nd โ๐) โ โค โ (2nd
โ๐) โ
โ) |
49 | 47, 48 | syl 17 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (2nd โ๐) โ
โ) |
50 | | qirropth 41260 |
. . . . . . 7
โข
(((โโ((๐ดโ2) โ 1)) โ (โ โ
โ) โง ((1st โ๐) โ โ โง (2nd
โ๐) โ โ)
โง ((1st โ๐) โ โ โง (2nd
โ๐) โ โ))
โ (((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ ((1st โ๐) = (1st โ๐) โง (2nd โ๐) = (2nd โ๐)))) |
51 | 34, 38, 42, 45, 49, 50 | syl122anc 1380 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ ((1st โ๐) = (1st โ๐) โง (2nd โ๐) = (2nd โ๐)))) |
52 | 51 | biimpd 228 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ ((1st โ๐) = (1st โ๐) โง (2nd โ๐) = (2nd โ๐)))) |
53 | | xpopth 7967 |
. . . . . 6
โข ((๐ โ (โ0
ร โค) โง ๐
โ (โ0 ร โค)) โ (((1st
โ๐) = (1st
โ๐) โง
(2nd โ๐) =
(2nd โ๐))
โ ๐ = ๐)) |
54 | 53 | adantl 483 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (((1st โ๐) = (1st โ๐) โง (2nd
โ๐) = (2nd
โ๐)) โ ๐ = ๐)) |
55 | 52, 54 | sylibd 238 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))
โ ๐ = ๐)) |
56 | 32, 55 | sylbid 239 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ (โ0 ร โค)
โง ๐ โ
(โ0 ร โค))) โ (((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) = ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) โ ๐ = ๐)) |
57 | 56 | ralrimivva 3198 |
. 2
โข (๐ด โ
(โคโฅโ2) โ โ๐ โ (โ0 ร
โค)โ๐ โ
(โ0 ร โค)(((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) = ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) โ ๐ = ๐)) |
58 | | dff1o6 7226 |
. 2
โข ((๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))):(โ0 ร
โค)โ1-1-ontoโ{๐ โฃ โ๐ โ โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐))} โ ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) Fn (โ0 ร โค)
โง ran (๐ โ
(โ0 ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) = {๐ โฃ โ๐ โ โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐))} โง โ๐ โ (โ0
ร โค)โ๐
โ (โ0 ร โค)(((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) = ((๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ๐) โ ๐ = ๐))) |
59 | 4, 17, 57, 58 | syl3anbrc 1344 |
1
โข (๐ด โ
(โคโฅโ2) โ (๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))):(โ0 ร
โค)โ1-1-ontoโ{๐ โฃ โ๐ โ โ0 โ๐ โ โค ๐ = (๐ + ((โโ((๐ดโ2) โ 1)) ยท ๐))}) |