Step | Hyp | Ref
| Expression |
1 | | mapd1o.f |
. . . . . 6
β’ πΉ = (LFnlβπ) |
2 | 1 | fvexi 6906 |
. . . . 5
β’ πΉ β V |
3 | 2 | rabex 5333 |
. . . 4
β’ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)} β V |
4 | | eqid 2733 |
. . . 4
β’ (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) = (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) |
5 | 3, 4 | fnmpti 6694 |
. . 3
β’ (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) Fn π |
6 | | mapd1o.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
7 | | mapd1o.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
8 | | mapd1o.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
9 | | mapd1o.s |
. . . . . 6
β’ π = (LSubSpβπ) |
10 | | mapd1o.l |
. . . . . 6
β’ πΏ = (LKerβπ) |
11 | | mapd1o.o |
. . . . . 6
β’ π = ((ocHβπΎ)βπ) |
12 | | mapd1o.m |
. . . . . 6
β’ π = ((mapdβπΎ)βπ) |
13 | 7, 8, 9, 1, 10, 11, 12 | mapdfval 40546 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β π = (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)})) |
14 | 6, 13 | syl 17 |
. . . 4
β’ (π β π = (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)})) |
15 | 14 | fneq1d 6643 |
. . 3
β’ (π β (π Fn π β (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) Fn π)) |
16 | 5, 15 | mpbiri 258 |
. 2
β’ (π β π Fn π) |
17 | 2 | rabex 5333 |
. . . . . . 7
β’ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)} β V |
18 | | eqid 2733 |
. . . . . . 7
β’ (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) = (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) |
19 | 17, 18 | fnmpti 6694 |
. . . . . 6
β’ (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) Fn π |
20 | 7, 8, 9, 1, 10, 11, 12 | mapdfval 40546 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β π = (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)})) |
21 | 6, 20 | syl 17 |
. . . . . . 7
β’ (π β π = (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)})) |
22 | 21 | fneq1d 6643 |
. . . . . 6
β’ (π β (π Fn π β (π‘ β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π‘)}) Fn π)) |
23 | 19, 22 | mpbiri 258 |
. . . . 5
β’ (π β π Fn π) |
24 | | fvelrnb 6953 |
. . . . 5
β’ (π Fn π β (π‘ β ran π β βπ β π (πβπ) = π‘)) |
25 | 23, 24 | syl 17 |
. . . 4
β’ (π β (π‘ β ran π β βπ β π (πβπ) = π‘)) |
26 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΎ β HL β§ π β π»)) |
27 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π) |
28 | 7, 8, 9, 1, 10, 11, 12, 26, 27 | mapdval 40547 |
. . . . . . . 8
β’ ((π β§ π β π) β (πβπ) = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) |
29 | | mapd1o.d |
. . . . . . . . . 10
β’ π· = (LDualβπ) |
30 | | mapd1o.t |
. . . . . . . . . 10
β’ π = (LSubSpβπ·) |
31 | | mapd1o.c |
. . . . . . . . . 10
β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} |
32 | | eqid 2733 |
. . . . . . . . . 10
β’ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} |
33 | 7, 11, 8, 9, 1, 10,
29, 30, 31, 32, 26, 27 | lclkrs2 40459 |
. . . . . . . . 9
β’ ((π β§ π β π) β ({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π β§ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β πΆ)) |
34 | | elin 3965 |
. . . . . . . . . 10
β’ ({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β (π β© π« πΆ) β ({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π β§ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π« πΆ)) |
35 | 2 | rabex 5333 |
. . . . . . . . . . . 12
β’ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β V |
36 | 35 | elpw 4607 |
. . . . . . . . . . 11
β’ ({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π« πΆ β {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β πΆ) |
37 | 36 | anbi2i 624 |
. . . . . . . . . 10
β’ (({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π β§ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π« πΆ) β ({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π β§ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β πΆ)) |
38 | 34, 37 | bitr2i 276 |
. . . . . . . . 9
β’ (({π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β π β§ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β πΆ) β {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β (π β© π« πΆ)) |
39 | 33, 38 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π β π) β {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)} β (π β© π« πΆ)) |
40 | 28, 39 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π β π) β (πβπ) β (π β© π« πΆ)) |
41 | | eleq1 2822 |
. . . . . . 7
β’ ((πβπ) = π‘ β ((πβπ) β (π β© π« πΆ) β π‘ β (π β© π« πΆ))) |
42 | 40, 41 | syl5ibcom 244 |
. . . . . 6
β’ ((π β§ π β π) β ((πβπ) = π‘ β π‘ β (π β© π« πΆ))) |
43 | 42 | rexlimdva 3156 |
. . . . 5
β’ (π β (βπ β π (πβπ) = π‘ β π‘ β (π β© π« πΆ))) |
44 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π β π‘ (πβ(πΏβπ)) = βͺ
π β π‘ (πβ(πΏβπ)) |
45 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β (π β© π« πΆ)) β (πΎ β HL β§ π β π»)) |
46 | | inss1 4229 |
. . . . . . . . . 10
β’ (π β© π« πΆ) β π |
47 | 46 | sseli 3979 |
. . . . . . . . 9
β’ (π‘ β (π β© π« πΆ) β π‘ β π) |
48 | 47 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π‘ β (π β© π« πΆ)) β π‘ β π) |
49 | | inss2 4230 |
. . . . . . . . . . 11
β’ (π β© π« πΆ) β π« πΆ |
50 | 49 | sseli 3979 |
. . . . . . . . . 10
β’ (π‘ β (π β© π« πΆ) β π‘ β π« πΆ) |
51 | 50 | elpwid 4612 |
. . . . . . . . 9
β’ (π‘ β (π β© π« πΆ) β π‘ β πΆ) |
52 | 51 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π‘ β (π β© π« πΆ)) β π‘ β πΆ) |
53 | 7, 11, 8, 9, 1, 10,
29, 30, 31, 44, 45, 48, 52 | lcfr 40504 |
. . . . . . 7
β’ ((π β§ π‘ β (π β© π« πΆ)) β βͺ π β π‘ (πβ(πΏβπ)) β π) |
54 | 7, 11, 12, 8, 9, 1,
10, 29, 30, 31, 45, 48, 52, 44 | mapdrval 40566 |
. . . . . . 7
β’ ((π β§ π‘ β (π β© π« πΆ)) β (πββͺ
π β π‘ (πβ(πΏβπ))) = π‘) |
55 | | fveqeq2 6901 |
. . . . . . . 8
β’ (π = βͺ π β π‘ (πβ(πΏβπ)) β ((πβπ) = π‘ β (πββͺ
π β π‘ (πβ(πΏβπ))) = π‘)) |
56 | 55 | rspcev 3613 |
. . . . . . 7
β’
((βͺ π β π‘ (πβ(πΏβπ)) β π β§ (πββͺ
π β π‘ (πβ(πΏβπ))) = π‘) β βπ β π (πβπ) = π‘) |
57 | 53, 54, 56 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π‘ β (π β© π« πΆ)) β βπ β π (πβπ) = π‘) |
58 | 57 | ex 414 |
. . . . 5
β’ (π β (π‘ β (π β© π« πΆ) β βπ β π (πβπ) = π‘)) |
59 | 43, 58 | impbid 211 |
. . . 4
β’ (π β (βπ β π (πβπ) = π‘ β π‘ β (π β© π« πΆ))) |
60 | 25, 59 | bitrd 279 |
. . 3
β’ (π β (π‘ β ran π β π‘ β (π β© π« πΆ))) |
61 | 60 | eqrdv 2731 |
. 2
β’ (π β ran π = (π β© π« πΆ)) |
62 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ (π‘ β π β§ π’ β π)) β (πΎ β HL β§ π β π»)) |
63 | | simprl 770 |
. . . . 5
β’ ((π β§ (π‘ β π β§ π’ β π)) β π‘ β π) |
64 | | simprr 772 |
. . . . 5
β’ ((π β§ (π‘ β π β§ π’ β π)) β π’ β π) |
65 | 7, 8, 9, 12, 62, 63, 64 | mapd11 40558 |
. . . 4
β’ ((π β§ (π‘ β π β§ π’ β π)) β ((πβπ‘) = (πβπ’) β π‘ = π’)) |
66 | 65 | biimpd 228 |
. . 3
β’ ((π β§ (π‘ β π β§ π’ β π)) β ((πβπ‘) = (πβπ’) β π‘ = π’)) |
67 | 66 | ralrimivva 3201 |
. 2
β’ (π β βπ‘ β π βπ’ β π ((πβπ‘) = (πβπ’) β π‘ = π’)) |
68 | | dff1o6 7273 |
. 2
β’ (π:πβ1-1-ontoβ(π β© π« πΆ) β (π Fn π β§ ran π = (π β© π« πΆ) β§ βπ‘ β π βπ’ β π ((πβπ‘) = (πβπ’) β π‘ = π’))) |
69 | 16, 61, 67, 68 | syl3anbrc 1344 |
1
β’ (π β π:πβ1-1-ontoβ(π β© π« πΆ)) |