Step | Hyp | Ref
| Expression |
1 | | lcf1o.v |
. . . . . 6
β’ π = (Baseβπ) |
2 | 1 | fvexi 6860 |
. . . . 5
β’ π β V |
3 | 2 | mptex 7177 |
. . . 4
β’ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯)))) β V |
4 | | lcf1o.j |
. . . 4
β’ π½ = (π₯ β (π β { 0 }) β¦ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π₯})π£ = (π€ + (π Β· π₯))))) |
5 | 3, 4 | fnmpti 6648 |
. . 3
β’ π½ Fn (π β { 0 }) |
6 | 5 | a1i 11 |
. 2
β’ (π β π½ Fn (π β { 0 })) |
7 | | fvelrnb 6907 |
. . . . 5
β’ (π½ Fn (π β { 0 }) β (π β ran π½ β βπ§ β (π β { 0 })(π½βπ§) = π)) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β (π β ran π½ β βπ§ β (π β { 0 })(π½βπ§) = π)) |
9 | | lcf1o.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
10 | | lcf1o.o |
. . . . . . . . 9
β’ β₯ =
((ocHβπΎ)βπ) |
11 | | lcf1o.u |
. . . . . . . . 9
β’ π = ((DVecHβπΎ)βπ) |
12 | | lcf1o.a |
. . . . . . . . 9
β’ + =
(+gβπ) |
13 | | lcf1o.t |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
14 | | lcf1o.s |
. . . . . . . . 9
β’ π = (Scalarβπ) |
15 | | lcf1o.r |
. . . . . . . . 9
β’ π
= (Baseβπ) |
16 | | lcf1o.z |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
17 | | lcf1o.f |
. . . . . . . . 9
β’ πΉ = (LFnlβπ) |
18 | | lcf1o.l |
. . . . . . . . 9
β’ πΏ = (LKerβπ) |
19 | | lcf1o.d |
. . . . . . . . 9
β’ π· = (LDualβπ) |
20 | | lcf1o.q |
. . . . . . . . 9
β’ π = (0gβπ·) |
21 | | lcf1o.c |
. . . . . . . . 9
β’ πΆ = {π β πΉ β£ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ)} |
22 | | lcflo.k |
. . . . . . . . . 10
β’ (π β (πΎ β HL β§ π β π»)) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β (π β { 0 })) β (πΎ β HL β§ π β π»)) |
24 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π§ β (π β { 0 })) β π§ β (π β { 0 })) |
25 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 4, 23, 24 | lcfrlem8 40062 |
. . . . . . . 8
β’ ((π β§ π§ β (π β { 0 })) β (π½βπ§) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) |
26 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) |
27 | | sneq 4600 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π§ β {π¦} = {π§}) |
28 | 27 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β ( β₯ β{π¦}) = ( β₯ β{π§})) |
29 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π§ β (π Β· π¦) = (π Β· π§)) |
30 | 29 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π§ β (π€ + (π Β· π¦)) = (π€ + (π Β· π§))) |
31 | 30 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π§ β (π£ = (π€ + (π Β· π¦)) β π£ = (π€ + (π Β· π§)))) |
32 | 28, 31 | rexeqbidv 3319 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π§ β (βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦)) β βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) |
33 | 32 | riotabidv 7319 |
. . . . . . . . . . . . . 14
β’ (π¦ = π§ β (β©π β π
βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦))) = (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) |
34 | 33 | mpteq2dv 5211 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) |
35 | 34 | rspceeqv 3599 |
. . . . . . . . . . . 12
β’ ((π§ β (π β { 0 }) β§ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) β βπ¦ β (π β { 0 })(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦))))) |
36 | 24, 26, 35 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π β { 0 })) β βπ¦ β (π β { 0 })(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦))))) |
37 | 36 | olcd 873 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π β { 0 })) β ((πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) = π β¨ βπ¦ β (π β { 0 })(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦)))))) |
38 | 9, 10, 11, 1, 16, 12, 13, 17, 14, 15, 26, 23, 24 | dochflcl 39988 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π β { 0 })) β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β πΉ) |
39 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 21, 23, 38 | lcfl6 40013 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π β { 0 })) β ((π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β πΆ β ((πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) = π β¨ βπ¦ β (π β { 0 })(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π¦})π£ = (π€ + (π Β· π¦))))))) |
40 | 37, 39 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π§ β (π β { 0 })) β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β πΆ) |
41 | 9, 10, 11, 1, 16, 12, 13, 18, 14, 15, 26, 23, 24 | dochsnkr2cl 39987 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π β { 0 })) β π§ β (( β₯ β(πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) β { 0 })) |
42 | 9, 10, 11, 1, 16, 17, 18, 23, 38, 41 | dochsnkrlem3 39984 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π β { 0 })) β ( β₯
β( β₯ β(πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))))) = (πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) |
43 | 9, 10, 11, 1, 16, 17, 18, 23, 38, 41 | dochsnkrlem1 39982 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π β { 0 })) β ( β₯
β( β₯ β(πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))))) β π) |
44 | 42, 43 | eqnetrrd 3009 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π β { 0 })) β (πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) β π) |
45 | 9, 11, 22 | dvhlmod 39623 |
. . . . . . . . . . . . 13
β’ (π β π β LMod) |
46 | 45 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (π β { 0 })) β π β LMod) |
47 | 1, 17, 18, 19, 20, 46, 38 | lkr0f2 37673 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (π β { 0 })) β ((πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) = π β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) = π)) |
48 | 47 | necon3bid 2985 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π β { 0 })) β ((πΏβ(π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) β π β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β π)) |
49 | 44, 48 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π§ β (π β { 0 })) β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β π) |
50 | | eldifsn 4751 |
. . . . . . . . 9
β’ ((π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β (πΆ β {π}) β ((π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β πΆ β§ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β π)) |
51 | 40, 49, 50 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ π§ β (π β { 0 })) β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))) β (πΆ β {π})) |
52 | 25, 51 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π§ β (π β { 0 })) β (π½βπ§) β (πΆ β {π})) |
53 | | eleq1 2822 |
. . . . . . 7
β’ ((π½βπ§) = π β ((π½βπ§) β (πΆ β {π}) β π β (πΆ β {π}))) |
54 | 52, 53 | syl5ibcom 244 |
. . . . . 6
β’ ((π β§ π§ β (π β { 0 })) β ((π½βπ§) = π β π β (πΆ β {π}))) |
55 | 54 | rexlimdva 3149 |
. . . . 5
β’ (π β (βπ§ β (π β { 0 })(π½βπ§) = π β π β (πΆ β {π}))) |
56 | | eldifsn 4751 |
. . . . . . . 8
β’ (π β (πΆ β {π}) β (π β πΆ β§ π β π)) |
57 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π β πΆ β§ π β π)) β π β πΆ) |
58 | 45 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β π β LMod) |
59 | 21 | lcfl1lem 40004 |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ β (π β πΉ β§ ( β₯ β( β₯
β(πΏβπ))) = (πΏβπ))) |
60 | 59 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π β πΆ β π β πΉ) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β π β πΉ) |
62 | 1, 17, 18, 19, 20, 58, 61 | lkr0f2 37673 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β ((πΏβπ) = π β π = π)) |
63 | 62 | necon3bid 2985 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((πΏβπ) β π β π β π)) |
64 | 63 | biimprd 248 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β (π β π β (πΏβπ) β π)) |
65 | 64 | impr 456 |
. . . . . . . . . 10
β’ ((π β§ (π β πΆ β§ π β π)) β (πΏβπ) β π) |
66 | 65 | neneqd 2945 |
. . . . . . . . 9
β’ ((π β§ (π β πΆ β§ π β π)) β Β¬ (πΏβπ) = π) |
67 | 22 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΆ β§ π β π)) β (πΎ β HL β§ π β π»)) |
68 | 60 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β πΆ β§ π β π) β π β πΉ) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β πΆ β§ π β π)) β π β πΉ) |
70 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 21, 67, 69 | lcfl6 40013 |
. . . . . . . . . . . 12
β’ ((π β§ (π β πΆ β§ π β π)) β (π β πΆ β ((πΏβπ) = π β¨ βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))))) |
71 | 70 | biimpa 478 |
. . . . . . . . . . 11
β’ (((π β§ (π β πΆ β§ π β π)) β§ π β πΆ) β ((πΏβπ) = π β¨ βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) |
72 | 71 | ord 863 |
. . . . . . . . . 10
β’ (((π β§ (π β πΆ β§ π β π)) β§ π β πΆ) β (Β¬ (πΏβπ) = π β βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) |
73 | 72 | 3impia 1118 |
. . . . . . . . 9
β’ (((π β§ (π β πΆ β§ π β π)) β§ π β πΆ β§ Β¬ (πΏβπ) = π) β βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) |
74 | 57, 66, 73 | mpd3an23 1464 |
. . . . . . . 8
β’ ((π β§ (π β πΆ β§ π β π)) β βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) |
75 | 56, 74 | sylan2b 595 |
. . . . . . 7
β’ ((π β§ π β (πΆ β {π})) β βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) |
76 | | eqcom 2740 |
. . . . . . . . 9
β’ ((π½βπ§) = π β π = (π½βπ§)) |
77 | 22 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (πΆ β {π})) β§ π§ β (π β { 0 })) β (πΎ β HL β§ π β π»)) |
78 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β (πΆ β {π})) β§ π§ β (π β { 0 })) β π§ β (π β { 0 })) |
79 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 4, 77, 78 | lcfrlem8 40062 |
. . . . . . . . . 10
β’ (((π β§ π β (πΆ β {π})) β§ π§ β (π β { 0 })) β (π½βπ§) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§))))) |
80 | 79 | eqeq2d 2744 |
. . . . . . . . 9
β’ (((π β§ π β (πΆ β {π})) β§ π§ β (π β { 0 })) β (π = (π½βπ§) β π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) |
81 | 76, 80 | bitrid 283 |
. . . . . . . 8
β’ (((π β§ π β (πΆ β {π})) β§ π§ β (π β { 0 })) β ((π½βπ§) = π β π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) |
82 | 81 | rexbidva 3170 |
. . . . . . 7
β’ ((π β§ π β (πΆ β {π})) β (βπ§ β (π β { 0 })(π½βπ§) = π β βπ§ β (π β { 0 })π = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π§})π£ = (π€ + (π Β· π§)))))) |
83 | 75, 82 | mpbird 257 |
. . . . . 6
β’ ((π β§ π β (πΆ β {π})) β βπ§ β (π β { 0 })(π½βπ§) = π) |
84 | 83 | ex 414 |
. . . . 5
β’ (π β (π β (πΆ β {π}) β βπ§ β (π β { 0 })(π½βπ§) = π)) |
85 | 55, 84 | impbid 211 |
. . . 4
β’ (π β (βπ§ β (π β { 0 })(π½βπ§) = π β π β (πΆ β {π}))) |
86 | 8, 85 | bitrd 279 |
. . 3
β’ (π β (π β ran π½ β π β (πΆ β {π}))) |
87 | 86 | eqrdv 2731 |
. 2
β’ (π β ran π½ = (πΆ β {π})) |
88 | 22 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β (πΎ β HL β§ π β π»)) |
89 | | eqid 2733 |
. . . . 5
β’ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π‘})π£ = (π€ + (π Β· π‘)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π‘})π£ = (π€ + (π Β· π‘)))) |
90 | | eqid 2733 |
. . . . 5
β’ (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π’})π£ = (π€ + (π Β· π’)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π’})π£ = (π€ + (π Β· π’)))) |
91 | | simplrl 776 |
. . . . 5
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β π‘ β (π β { 0 })) |
92 | | simplrr 777 |
. . . . 5
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β π’ β (π β { 0 })) |
93 | | simpr 486 |
. . . . . 6
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β (π½βπ‘) = (π½βπ’)) |
94 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 4, 88, 91 | lcfrlem8 40062 |
. . . . . 6
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β (π½βπ‘) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π‘})π£ = (π€ + (π Β· π‘))))) |
95 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 4, 88, 92 | lcfrlem8 40062 |
. . . . . 6
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β (π½βπ’) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π’})π£ = (π€ + (π Β· π’))))) |
96 | 93, 94, 95 | 3eqtr3d 2781 |
. . . . 5
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π‘})π£ = (π€ + (π Β· π‘)))) = (π£ β π β¦ (β©π β π
βπ€ β ( β₯ β{π’})π£ = (π€ + (π Β· π’))))) |
97 | 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 88, 89, 90, 91, 92, 96 | lcfl7lem 40012 |
. . . 4
β’ (((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β§ (π½βπ‘) = (π½βπ’)) β π‘ = π’) |
98 | 97 | ex 414 |
. . 3
β’ ((π β§ (π‘ β (π β { 0 }) β§ π’ β (π β { 0 }))) β ((π½βπ‘) = (π½βπ’) β π‘ = π’)) |
99 | 98 | ralrimivva 3194 |
. 2
β’ (π β βπ‘ β (π β { 0 })βπ’ β (π β { 0 })((π½βπ‘) = (π½βπ’) β π‘ = π’)) |
100 | | dff1o6 7225 |
. 2
β’ (π½:(π β { 0 })β1-1-ontoβ(πΆ β {π}) β (π½ Fn (π β { 0 }) β§ ran π½ = (πΆ β {π}) β§ βπ‘ β (π β { 0 })βπ’ β (π β { 0 })((π½βπ‘) = (π½βπ’) β π‘ = π’))) |
101 | 6, 87, 99, 100 | syl3anbrc 1344 |
1
β’ (π β π½:(π β { 0 })β1-1-ontoβ(πΆ β {π})) |