Step | Hyp | Ref
| Expression |
1 | | smfinfmpt.g |
. . . 4
β’ πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ π΅), β, < )) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΊ = (π₯ β π· β¦ inf(ran (π β π β¦ π΅), β, < ))) |
3 | | smfinfmpt.x |
. . . . 5
β’
β²π₯π |
4 | | smfinfmpt.d |
. . . . . . 7
β’ π· = {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} |
5 | 4 | a1i 11 |
. . . . . 6
β’ (π β π· = {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅}) |
6 | | smfinfmpt.n |
. . . . . . . . 9
β’
β²ππ |
7 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ (π β (π β π β¦ (π₯ β π΄ β¦ π΅)) = (π β π β¦ (π₯ β π΄ β¦ π΅))) |
8 | | smfinfmpt.f |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) |
9 | 7, 8 | fvmpt2d 7012 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) = (π₯ β π΄ β¦ π΅)) |
10 | 9 | dmeqd 5906 |
. . . . . . . . . 10
β’ ((π β§ π β π) β dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) = dom (π₯ β π΄ β¦ π΅)) |
11 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯π |
12 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯π |
13 | 11, 12 | nfel 2918 |
. . . . . . . . . . . 12
β’
β²π₯ π β π |
14 | 3, 13 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π₯(π β§ π β π) |
15 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
16 | | smfinfmpt.s |
. . . . . . . . . . . . . 14
β’ (π β π β SAlg) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β SAlg) |
18 | | smfinfmpt.b |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π β§ π₯ β π΄) β π΅ β π) |
19 | 18 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π₯ β π΄) β π΅ β π) |
20 | 14, 17, 19, 8 | smffmpt 45521 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
21 | 20 | fvmptelcdm 7113 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π₯ β π΄) β π΅ β β) |
22 | 14, 15, 21 | dmmptdf 43923 |
. . . . . . . . . 10
β’ ((π β§ π β π) β dom (π₯ β π΄ β¦ π΅) = π΄) |
23 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π΄ = π΄) |
24 | 10, 22, 23 | 3eqtrrd 2778 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΄ = dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) |
25 | 6, 24 | iineq2d 5021 |
. . . . . . . 8
β’ (π β β© π β π π΄ = β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) |
26 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯β© π β π π΄ |
27 | | nfmpt1 5257 |
. . . . . . . . . . . . 13
β’
β²π₯(π₯ β π΄ β¦ π΅) |
28 | 12, 27 | nfmpt 5256 |
. . . . . . . . . . . 12
β’
β²π₯(π β π β¦ (π₯ β π΄ β¦ π΅)) |
29 | 28, 11 | nffv 6902 |
. . . . . . . . . . 11
β’
β²π₯((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) |
30 | 29 | nfdm 5951 |
. . . . . . . . . 10
β’
β²π₯dom
((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) |
31 | 12, 30 | nfiin 5029 |
. . . . . . . . 9
β’
β²π₯β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) |
32 | 26, 31 | rabeqf 3467 |
. . . . . . . 8
β’ (β© π β π π΄ = β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ π΅}) |
33 | 25, 32 | syl 17 |
. . . . . . 7
β’ (π β {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ π΅}) |
34 | | smfinfmpt.y |
. . . . . . . . . 10
β’
β²π¦π |
35 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦ π₯ β β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) |
36 | 34, 35 | nfan 1903 |
. . . . . . . . 9
β’
β²π¦(π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) |
37 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ₯ |
38 | | nfii1 5033 |
. . . . . . . . . . . 12
β’
β²πβ© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) |
39 | 37, 38 | nfel 2918 |
. . . . . . . . . . 11
β’
β²π π₯ β β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) |
40 | 6, 39 | nfan 1903 |
. . . . . . . . . 10
β’
β²π(π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) |
41 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β§ π β π) β π) |
42 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β§ π β π) β π β π) |
43 | | eliinid 43800 |
. . . . . . . . . . . . 13
β’ ((π₯ β β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β§ π β π) β π₯ β dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) |
44 | 43 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β§ π β π) β π₯ β dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) |
45 | 24 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) = π΄) |
46 | 45 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β§ π β π) β dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) = π΄) |
47 | 44, 46 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β§ π β π) β π₯ β π΄) |
48 | 9 | fveq1d 6894 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯) = ((π₯ β π΄ β¦ π΅)βπ₯)) |
49 | 48 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π₯ β π΄) β (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯) = ((π₯ β π΄ β¦ π΅)βπ₯)) |
50 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π β§ π₯ β π΄) β π₯ β π΄) |
51 | 15 | fvmpt2 7010 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π΄ β§ π΅ β π) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
52 | 50, 18, 51 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
53 | 49, 52 | eqtr2d 2774 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π₯ β π΄) β π΅ = (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)) |
54 | 53 | breq2d 5161 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ π₯ β π΄) β (π¦ β€ π΅ β π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯))) |
55 | 41, 42, 47, 54 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β§ π β π) β (π¦ β€ π΅ β π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯))) |
56 | 40, 55 | ralbida 3268 |
. . . . . . . . 9
β’ ((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β (βπ β π π¦ β€ π΅ β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯))) |
57 | 36, 56 | rexbid 3272 |
. . . . . . . 8
β’ ((π β§ π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)) β (βπ¦ β β βπ β π π¦ β€ π΅ β βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯))) |
58 | 3, 57 | rabbida 3459 |
. . . . . . 7
β’ (π β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ π΅} = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)}) |
59 | 33, 58 | eqtrd 2773 |
. . . . . 6
β’ (π β {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)}) |
60 | 5, 59 | eqtrd 2773 |
. . . . 5
β’ (π β π· = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)}) |
61 | 3, 60 | alrimi 2207 |
. . . 4
β’ (π β βπ₯ π· = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)}) |
62 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²πβ |
63 | | nfra1 3282 |
. . . . . . . . . . . . . 14
β’
β²πβπ β π π¦ β€ π΅ |
64 | 62, 63 | nfrexw 3311 |
. . . . . . . . . . . . 13
β’
β²πβπ¦ β β βπ β π π¦ β€ π΅ |
65 | | nfii1 5033 |
. . . . . . . . . . . . 13
β’
β²πβ© π β π π΄ |
66 | 64, 65 | nfrabw 3469 |
. . . . . . . . . . . 12
β’
β²π{π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} |
67 | 4, 66 | nfcxfr 2902 |
. . . . . . . . . . 11
β’
β²ππ· |
68 | 37, 67 | nfel 2918 |
. . . . . . . . . 10
β’
β²π π₯ β π· |
69 | 6, 68 | nfan 1903 |
. . . . . . . . 9
β’
β²π(π β§ π₯ β π·) |
70 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β π) β π) |
71 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β π) β π β π) |
72 | 4 | eleq2i 2826 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π· β π₯ β {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅}) |
73 | 72 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ (π₯ β π· β π₯ β {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅}) |
74 | | rabidim1 3454 |
. . . . . . . . . . . . . 14
β’ (π₯ β {π₯ β β©
π β π π΄ β£ βπ¦ β β βπ β π π¦ β€ π΅} β π₯ β β©
π β π π΄) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β π· β π₯ β β©
π β π π΄) |
76 | 75 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π₯ β π· β§ π β π) β π₯ β β©
π β π π΄) |
77 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ β π· β§ π β π) β π β π) |
78 | | eliinid 43800 |
. . . . . . . . . . . 12
β’ ((π₯ β β© π β π π΄ β§ π β π) β π₯ β π΄) |
79 | 76, 77, 78 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π₯ β π· β§ π β π) β π₯ β π΄) |
80 | 79 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β π) β π₯ β π΄) |
81 | 53 | idi 1 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ π₯ β π΄) β π΅ = (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)) |
82 | 70, 71, 80, 81 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β π) β π΅ = (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)) |
83 | 69, 82 | mpteq2da 5247 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β (π β π β¦ π΅) = (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯))) |
84 | 83 | rneqd 5938 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β ran (π β π β¦ π΅) = ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯))) |
85 | 84 | infeq1d 9472 |
. . . . . 6
β’ ((π β§ π₯ β π·) β inf(ran (π β π β¦ π΅), β, < ) = inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < )) |
86 | 85 | ex 414 |
. . . . 5
β’ (π β (π₯ β π· β inf(ran (π β π β¦ π΅), β, < ) = inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < ))) |
87 | 3, 86 | ralrimi 3255 |
. . . 4
β’ (π β βπ₯ β π· inf(ran (π β π β¦ π΅), β, < ) = inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < )) |
88 | | mpteq12f 5237 |
. . . 4
β’
((βπ₯ π· = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β§ βπ₯ β π· inf(ran (π β π β¦ π΅), β, < ) = inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < )) β (π₯ β π· β¦ inf(ran (π β π β¦ π΅), β, < )) = (π₯ β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β¦ inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < ))) |
89 | 61, 87, 88 | syl2anc 585 |
. . 3
β’ (π β (π₯ β π· β¦ inf(ran (π β π β¦ π΅), β, < )) = (π₯ β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β¦ inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < ))) |
90 | 2, 89 | eqtrd 2773 |
. 2
β’ (π β πΊ = (π₯ β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β¦ inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < ))) |
91 | | nfmpt1 5257 |
. . 3
β’
β²π(π β π β¦ (π₯ β π΄ β¦ π΅)) |
92 | | smfinfmpt.m |
. . 3
β’ (π β π β β€) |
93 | | smfinfmpt.z |
. . 3
β’ π =
(β€β₯βπ) |
94 | | eqid 2733 |
. . . 4
β’ (π β π β¦ (π₯ β π΄ β¦ π΅)) = (π β π β¦ (π₯ β π΄ β¦ π΅)) |
95 | 6, 8, 94 | fmptdf 7117 |
. . 3
β’ (π β (π β π β¦ (π₯ β π΄ β¦ π΅)):πβΆ(SMblFnβπ)) |
96 | | eqid 2733 |
. . 3
β’ {π₯ β β© π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} = {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} |
97 | | eqid 2733 |
. . 3
β’ (π₯ β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β¦ inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < )) = (π₯ β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β¦ inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < )) |
98 | 91, 28, 92, 93, 16, 95, 96, 97 | smfinf 45534 |
. 2
β’ (π β (π₯ β {π₯ β β©
π β π dom ((π β π β¦ (π₯ β π΄ β¦ π΅))βπ) β£ βπ¦ β β βπ β π π¦ β€ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)} β¦ inf(ran (π β π β¦ (((π β π β¦ (π₯ β π΄ β¦ π΅))βπ)βπ₯)), β, < )) β
(SMblFnβπ)) |
99 | 90, 98 | eqeltrd 2834 |
1
β’ (π β πΊ β (SMblFnβπ)) |