Step | Hyp | Ref
| Expression |
1 | | lincext.f |
. 2
β’ πΉ = (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) |
2 | | lincext.r |
. . . . . . . 8
β’ π
= (Scalarβπ) |
3 | | eqid 2733 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
4 | 3 | lmodfgrp 20374 |
. . . . . . . . 9
β’ (π β LMod β
(Scalarβπ) β
Grp) |
5 | 4 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (Scalarβπ) β Grp) |
6 | 2, 5 | eqeltrid 2838 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β π
β Grp) |
7 | | simpr1 1195 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β π β πΈ) |
8 | | lincext.e |
. . . . . . . 8
β’ πΈ = (Baseβπ
) |
9 | | lincext.n |
. . . . . . . 8
β’ π = (invgβπ
) |
10 | 8, 9 | grpinvcl 18806 |
. . . . . . 7
β’ ((π
β Grp β§ π β πΈ) β (πβπ) β πΈ) |
11 | 6, 7, 10 | syl2anc 585 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (πβπ) β πΈ) |
12 | 11 | ad2antrr 725 |
. . . . 5
β’
(((((π β LMod
β§ π β π«
π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β§ π§ β π) β§ π§ = π) β (πβπ) β πΈ) |
13 | | elmapi 8793 |
. . . . . . . . 9
β’ (πΊ β (πΈ βm (π β {π})) β πΊ:(π β {π})βΆπΈ) |
14 | | df-ne 2941 |
. . . . . . . . . . . . . 14
β’ (π§ β π β Β¬ π§ = π) |
15 | 14 | biimpri 227 |
. . . . . . . . . . . . 13
β’ (Β¬
π§ = π β π§ β π) |
16 | 15 | anim2i 618 |
. . . . . . . . . . . 12
β’ ((π§ β π β§ Β¬ π§ = π) β (π§ β π β§ π§ β π)) |
17 | | eldifsn 4751 |
. . . . . . . . . . . 12
β’ (π§ β (π β {π}) β (π§ β π β§ π§ β π)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π§ β π β§ Β¬ π§ = π) β π§ β (π β {π})) |
19 | | ffvelcdm 7036 |
. . . . . . . . . . 11
β’ ((πΊ:(π β {π})βΆπΈ β§ π§ β (π β {π})) β (πΊβπ§) β πΈ) |
20 | 18, 19 | sylan2 594 |
. . . . . . . . . 10
β’ ((πΊ:(π β {π})βΆπΈ β§ (π§ β π β§ Β¬ π§ = π)) β (πΊβπ§) β πΈ) |
21 | 20 | ex 414 |
. . . . . . . . 9
β’ (πΊ:(π β {π})βΆπΈ β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
22 | 13, 21 | syl 17 |
. . . . . . . 8
β’ (πΊ β (πΈ βm (π β {π})) β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
23 | 22 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π}))) β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
24 | 23 | adantl 483 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
25 | 24 | impl 457 |
. . . . 5
β’
(((((π β LMod
β§ π β π«
π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β§ π§ β π) β§ Β¬ π§ = π) β (πΊβπ§) β πΈ) |
26 | 12, 25 | ifclda 4525 |
. . . 4
β’ ((((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β§ π§ β π) β if(π§ = π, (πβπ), (πΊβπ§)) β πΈ) |
27 | 26 | fmpttd 7067 |
. . 3
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))):πβΆπΈ) |
28 | | simpr 486 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅) β π β π« π΅) |
29 | 8 | fvexi 6860 |
. . . . . 6
β’ πΈ β V |
30 | 28, 29 | jctil 521 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β (πΈ β V β§ π β π« π΅)) |
31 | 30 | adantr 482 |
. . . 4
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (πΈ β V β§ π β π« π΅)) |
32 | | elmapg 8784 |
. . . 4
β’ ((πΈ β V β§ π β π« π΅) β ((π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β (πΈ βm π) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))):πβΆπΈ)) |
33 | 31, 32 | syl 17 |
. . 3
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β ((π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β (πΈ βm π) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))):πβΆπΈ)) |
34 | 27, 33 | mpbird 257 |
. 2
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β (πΈ βm π)) |
35 | 1, 34 | eqeltrid 2838 |
1
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β πΉ β (πΈ βm π)) |