Step | Hyp | Ref
| Expression |
1 | | esumiun.0 |
. . . 4
β’ (π β π΄ β π) |
2 | | esumiun.1 |
. . . 4
β’ ((π β§ π β π΄) β π΅ β π) |
3 | 1, 2 | aciunf1 31621 |
. . 3
β’ (π β βπ(π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β§ βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π)) |
4 | | f1f1orn 6800 |
. . . . . 6
β’ (π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β π:βͺ π β π΄ π΅β1-1-ontoβran
π) |
5 | 4 | anim1i 616 |
. . . . 5
β’ ((π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β§ βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) β (π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π)) |
6 | | f1f 6743 |
. . . . . . 7
β’ (π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β π:βͺ π β π΄ π΅βΆβͺ
π β π΄ ({π} Γ π΅)) |
7 | 6 | frnd 6681 |
. . . . . 6
β’ (π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β ran π β βͺ
π β π΄ ({π} Γ π΅)) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β§ βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) β ran π β βͺ
π β π΄ ({π} Γ π΅)) |
9 | 5, 8 | jca 513 |
. . . 4
β’ ((π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β§ βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) β ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) |
10 | 9 | eximi 1838 |
. . 3
β’
(βπ(π:βͺ π β π΄ π΅β1-1ββͺ π β π΄ ({π} Γ π΅) β§ βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) β βπ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) |
11 | 3, 10 | syl 17 |
. 2
β’ (π β βπ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) |
12 | | nfv 1918 |
. . . . . 6
β’
β²π§(π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) |
13 | | nfcv 2908 |
. . . . . 6
β’
β²π§πΆ |
14 | | nfcsb1v 3885 |
. . . . . 6
β’
β²πβ¦(2nd βπ§) / πβ¦πΆ |
15 | | nfcv 2908 |
. . . . . 6
β’
β²π§βͺ π β π΄ π΅ |
16 | | nfcv 2908 |
. . . . . 6
β’
β²π§ran
π |
17 | | nfcv 2908 |
. . . . . 6
β’
β²π§β‘π |
18 | | csbeq1a 3874 |
. . . . . 6
β’ (π = (2nd βπ§) β πΆ = β¦(2nd
βπ§) / πβ¦πΆ) |
19 | 2 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β π΄ π΅ β π) |
20 | | iunexg 7901 |
. . . . . . . 8
β’ ((π΄ β π β§ βπ β π΄ π΅ β π) β βͺ
π β π΄ π΅ β V) |
21 | 1, 19, 20 | syl2anc 585 |
. . . . . . 7
β’ (π β βͺ π β π΄ π΅ β V) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β βͺ π β π΄ π΅ β V) |
23 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ ran π β βͺ π β π΄ ({π} Γ π΅))) β π:βͺ π β π΄ π΅β1-1-ontoβran
π) |
24 | | f1ocnv 6801 |
. . . . . . . 8
β’ (π:βͺ π β π΄ π΅β1-1-ontoβran
π β β‘π:ran πβ1-1-ontoββͺ π β π΄ π΅) |
25 | 23, 24 | syl 17 |
. . . . . . 7
β’ ((π β§ (π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ ran π β βͺ π β π΄ ({π} Γ π΅))) β β‘π:ran πβ1-1-ontoββͺ π β π΄ π΅) |
26 | 25 | adantrlr 722 |
. . . . . 6
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β β‘π:ran πβ1-1-ontoββͺ π β π΄ π΅) |
27 | | nfv 1918 |
. . . . . . . . 9
β’
β²ππ |
28 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²ππ |
29 | | nfiu1 4993 |
. . . . . . . . . . . 12
β’
β²πβͺ π β π΄ π΅ |
30 | 28 | nfrn 5912 |
. . . . . . . . . . . 12
β’
β²πran
π |
31 | 28, 29, 30 | nff1o 6787 |
. . . . . . . . . . 11
β’
β²π π:βͺ π β π΄ π΅β1-1-ontoβran
π |
32 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π(2nd β(πβπ)) = π |
33 | 29, 32 | nfralw 3297 |
. . . . . . . . . . 11
β’
β²πβπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π |
34 | 31, 33 | nfan 1903 |
. . . . . . . . . 10
β’
β²π(π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) |
35 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²πran
π |
36 | | nfiu1 4993 |
. . . . . . . . . . 11
β’
β²πβͺ π β π΄ ({π} Γ π΅) |
37 | 35, 36 | nfss 3941 |
. . . . . . . . . 10
β’
β²πran π β βͺ π β π΄ ({π} Γ π΅) |
38 | 34, 37 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅)) |
39 | 27, 38 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) |
40 | | nfv 1918 |
. . . . . . . 8
β’
β²π π§ β ran π |
41 | 39, 40 | nfan 1903 |
. . . . . . 7
β’
β²π((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) |
42 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (πβπ) = π§) |
43 | 42 | fveq2d 6851 |
. . . . . . . . . 10
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (2nd β(πβπ)) = (2nd βπ§)) |
44 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β π β βͺ
π β π΄ π΅) |
45 | | simp-4r 783 |
. . . . . . . . . . . . . 14
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) |
46 | 45 | simpld 496 |
. . . . . . . . . . . . 13
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β (π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π)) |
47 | 46 | simprd 497 |
. . . . . . . . . . . 12
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) |
49 | | 2fveq3 6852 |
. . . . . . . . . . . . 13
β’ (π = π β (2nd β(πβπ)) = (2nd β(πβπ))) |
50 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = π β π = π) |
51 | 49, 50 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (π = π β ((2nd β(πβπ)) = π β (2nd β(πβπ)) = π)) |
52 | 51 | rspcva 3582 |
. . . . . . . . . . 11
β’ ((π β βͺ π β π΄ π΅ β§ βπ β βͺ
π β π΄ π΅(2nd β(πβπ)) = π) β (2nd β(πβπ)) = π) |
53 | 44, 48, 52 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (2nd β(πβπ)) = π) |
54 | 43, 53 | eqtr3d 2779 |
. . . . . . . . 9
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (2nd βπ§) = π) |
55 | 46 | simpld 496 |
. . . . . . . . . . 11
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β π:βͺ π β π΄ π΅β1-1-ontoβran
π) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β π:βͺ π β π΄ π΅β1-1-ontoβran
π) |
57 | | f1ocnvfv1 7227 |
. . . . . . . . . 10
β’ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ π β βͺ
π β π΄ π΅) β (β‘πβ(πβπ)) = π) |
58 | 56, 44, 57 | syl2anc 585 |
. . . . . . . . 9
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (β‘πβ(πβπ)) = π) |
59 | 42 | fveq2d 6851 |
. . . . . . . . 9
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (β‘πβ(πβπ)) = (β‘πβπ§)) |
60 | 54, 58, 59 | 3eqtr2rd 2784 |
. . . . . . . 8
β’
(((((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β§ π β βͺ
π β π΄ π΅) β§ (πβπ) = π§) β (β‘πβπ§) = (2nd βπ§)) |
61 | | f1ofn 6790 |
. . . . . . . . . 10
β’ (π:βͺ π β π΄ π΅β1-1-ontoβran
π β π Fn βͺ π β π΄ π΅) |
62 | 55, 61 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β π Fn βͺ π β π΄ π΅) |
63 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β π§ β ran π) |
64 | | fvelrnb 6908 |
. . . . . . . . . 10
β’ (π Fn βͺ π β π΄ π΅ β (π§ β ran π β βπ β βͺ
π β π΄ π΅(πβπ) = π§)) |
65 | 64 | biimpa 478 |
. . . . . . . . 9
β’ ((π Fn βͺ π β π΄ π΅ β§ π§ β ran π) β βπ β βͺ
π β π΄ π΅(πβπ) = π§) |
66 | 62, 63, 65 | syl2anc 585 |
. . . . . . . 8
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β βπ β βͺ
π β π΄ π΅(πβπ) = π§) |
67 | 60, 66 | r19.29a 3160 |
. . . . . . 7
β’
(((((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β§ π β π΄) β§ π§ β ({π} Γ π΅)) β (β‘πβπ§) = (2nd βπ§)) |
68 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β ran π β βͺ
π β π΄ ({π} Γ π΅)) |
69 | 68 | sselda 3949 |
. . . . . . . 8
β’ (((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β π§ β βͺ
π β π΄ ({π} Γ π΅)) |
70 | | eliun 4963 |
. . . . . . . 8
β’ (π§ β βͺ π β π΄ ({π} Γ π΅) β βπ β π΄ π§ β ({π} Γ π΅)) |
71 | 69, 70 | sylib 217 |
. . . . . . 7
β’ (((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β βπ β π΄ π§ β ({π} Γ π΅)) |
72 | 41, 67, 71 | r19.29af 3254 |
. . . . . 6
β’ (((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β ran π) β (β‘πβπ§) = (2nd βπ§)) |
73 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ |
74 | 73, 29 | nfel 2922 |
. . . . . . . . 9
β’
β²π π β βͺ π β π΄ π΅ |
75 | 27, 74 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ π β βͺ
π β π΄ π΅) |
76 | | esumiun.2 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π β π΅) β πΆ β (0[,]+β)) |
77 | 76 | adantllr 718 |
. . . . . . . 8
β’ ((((π β§ π β βͺ
π β π΄ π΅) β§ π β π΄) β§ π β π΅) β πΆ β (0[,]+β)) |
78 | | eliun 4963 |
. . . . . . . . . 10
β’ (π β βͺ π β π΄ π΅ β βπ β π΄ π β π΅) |
79 | 78 | biimpi 215 |
. . . . . . . . 9
β’ (π β βͺ π β π΄ π΅ β βπ β π΄ π β π΅) |
80 | 79 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β βͺ
π β π΄ π΅) β βπ β π΄ π β π΅) |
81 | 75, 77, 80 | r19.29af 3254 |
. . . . . . 7
β’ ((π β§ π β βͺ
π β π΄ π΅) β πΆ β (0[,]+β)) |
82 | 81 | adantlr 714 |
. . . . . 6
β’ (((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π β βͺ
π β π΄ π΅) β πΆ β (0[,]+β)) |
83 | 12, 13, 14, 15, 16, 17, 18, 22, 26, 72, 82 | esumf1o 32689 |
. . . . 5
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β Ξ£*π β βͺ π β π΄ π΅πΆ = Ξ£*π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ) |
84 | 83 | eqcomd 2743 |
. . . 4
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β Ξ£*π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ = Ξ£*π β βͺ
π β π΄ π΅πΆ) |
85 | | vsnex 5391 |
. . . . . . . . . 10
β’ {π} β V |
86 | 85 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β {π} β V) |
87 | 86, 2 | xpexd 7690 |
. . . . . . . 8
β’ ((π β§ π β π΄) β ({π} Γ π΅) β V) |
88 | 87 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ β π΄ ({π} Γ π΅) β V) |
89 | | iunexg 7901 |
. . . . . . 7
β’ ((π΄ β π β§ βπ β π΄ ({π} Γ π΅) β V) β βͺ π β π΄ ({π} Γ π΅) β V) |
90 | 1, 88, 89 | syl2anc 585 |
. . . . . 6
β’ (π β βͺ π β π΄ ({π} Γ π΅) β V) |
91 | 90 | adantr 482 |
. . . . 5
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β βͺ π β π΄ ({π} Γ π΅) β V) |
92 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππ§ |
93 | 92, 36 | nfel 2922 |
. . . . . . . 8
β’
β²π π§ β βͺ π β π΄ ({π} Γ π΅) |
94 | 27, 93 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) |
95 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(2nd βπ§) |
96 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππΆ |
97 | 95, 96 | nfcsbw 3887 |
. . . . . . . 8
β’
β²πβ¦(2nd βπ§) / πβ¦πΆ |
98 | | nfcv 2908 |
. . . . . . . 8
β’
β²π(0[,]+β) |
99 | 97, 98 | nfel 2922 |
. . . . . . 7
β’
β²πβ¦(2nd βπ§) / πβ¦πΆ β (0[,]+β) |
100 | | simprr 772 |
. . . . . . . 8
β’ ((((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β§ π β π΄) β§ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) β (2nd βπ§) β π΅) |
101 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β§ π β π΄) β§ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) β π) |
102 | | simplr 768 |
. . . . . . . . 9
β’ ((((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β§ π β π΄) β§ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) β π β π΄) |
103 | 76 | ralrimiva 3144 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β βπ β π΅ πΆ β (0[,]+β)) |
104 | 101, 102,
103 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β§ π β π΄) β§ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) β βπ β π΅ πΆ β (0[,]+β)) |
105 | | rspcsbela 4400 |
. . . . . . . 8
β’
(((2nd βπ§) β π΅ β§ βπ β π΅ πΆ β (0[,]+β)) β
β¦(2nd βπ§) / πβ¦πΆ β (0[,]+β)) |
106 | 100, 104,
105 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β§ π β π΄) β§ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) β β¦(2nd
βπ§) / πβ¦πΆ β (0[,]+β)) |
107 | | xp1st 7958 |
. . . . . . . . . . . 12
β’ (π§ β ({π} Γ π΅) β (1st βπ§) β {π}) |
108 | | elsni 4608 |
. . . . . . . . . . . 12
β’
((1st βπ§) β {π} β (1st βπ§) = π) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . 11
β’ (π§ β ({π} Γ π΅) β (1st βπ§) = π) |
110 | | xp2nd 7959 |
. . . . . . . . . . 11
β’ (π§ β ({π} Γ π΅) β (2nd βπ§) β π΅) |
111 | 109, 110 | jca 513 |
. . . . . . . . . 10
β’ (π§ β ({π} Γ π΅) β ((1st βπ§) = π β§ (2nd βπ§) β π΅)) |
112 | 111 | reximi 3088 |
. . . . . . . . 9
β’
(βπ β
π΄ π§ β ({π} Γ π΅) β βπ β π΄ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) |
113 | 70, 112 | sylbi 216 |
. . . . . . . 8
β’ (π§ β βͺ π β π΄ ({π} Γ π΅) β βπ β π΄ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) |
114 | 113 | adantl 483 |
. . . . . . 7
β’ ((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β βπ β π΄ ((1st βπ§) = π β§ (2nd βπ§) β π΅)) |
115 | 94, 99, 106, 114 | r19.29af2 3253 |
. . . . . 6
β’ ((π β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β β¦(2nd
βπ§) / πβ¦πΆ β (0[,]+β)) |
116 | 115 | adantlr 714 |
. . . . 5
β’ (((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β§ π§ β βͺ
π β π΄ ({π} Γ π΅)) β β¦(2nd
βπ§) / πβ¦πΆ β (0[,]+β)) |
117 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ ran π β βͺ π β π΄ ({π} Γ π΅))) β ran π β βͺ
π β π΄ ({π} Γ π΅)) |
118 | 117 | adantrlr 722 |
. . . . 5
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β ran π β βͺ
π β π΄ ({π} Γ π΅)) |
119 | 12, 91, 116, 118 | esummono 32693 |
. . . 4
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β Ξ£*π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ β€ Ξ£*π§ β βͺ
π β π΄ ({π} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
120 | 84, 119 | eqbrtrrd 5134 |
. . 3
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β Ξ£*π β βͺ π β π΄ π΅πΆ β€ Ξ£*π§ β βͺ
π β π΄ ({π} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
121 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
122 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
123 | 121, 122 | op2ndd 7937 |
. . . . . . . 8
β’ (π§ = β¨π, πβ© β (2nd βπ§) = π) |
124 | 123 | eqcomd 2743 |
. . . . . . 7
β’ (π§ = β¨π, πβ© β π = (2nd βπ§)) |
125 | 124, 18 | syl 17 |
. . . . . 6
β’ (π§ = β¨π, πβ© β πΆ = β¦(2nd
βπ§) / πβ¦πΆ) |
126 | 125 | eqcomd 2743 |
. . . . 5
β’ (π§ = β¨π, πβ© β β¦(2nd
βπ§) / πβ¦πΆ = πΆ) |
127 | 76 | anasss 468 |
. . . . 5
β’ ((π β§ (π β π΄ β§ π β π΅)) β πΆ β (0[,]+β)) |
128 | 14, 126, 1, 2, 127 | esum2d 32732 |
. . . 4
β’ (π β Ξ£*π β π΄Ξ£*π β π΅πΆ = Ξ£*π§ β βͺ
π β π΄ ({π} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
129 | 128 | adantr 482 |
. . 3
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β Ξ£*π β π΄Ξ£*π β π΅πΆ = Ξ£*π§ β βͺ
π β π΄ ({π} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
130 | 120, 129 | breqtrrd 5138 |
. 2
β’ ((π β§ ((π:βͺ π β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π β π΄ ({π} Γ π΅))) β Ξ£*π β βͺ π β π΄ π΅πΆ β€ Ξ£*π β π΄Ξ£*π β π΅πΆ) |
131 | 11, 130 | exlimddv 1939 |
1
β’ (π β Ξ£*π β βͺ π β π΄ π΅πΆ β€ Ξ£*π β π΄Ξ£*π β π΅πΆ) |