Step | Hyp | Ref
| Expression |
1 | | lincext.f |
. 2
β’ πΉ = (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) |
2 | | lincext.r |
. . . . . . . 8
β’ π
= (Scalarβπ) |
3 | | eqid 2732 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
4 | 3 | lmodfgrp 20484 |
. . . . . . . . 9
β’ (π β LMod β
(Scalarβπ) β
Grp) |
5 | 4 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (Scalarβπ) β Grp) |
6 | 2, 5 | eqeltrid 2837 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β π
β Grp) |
7 | | simpr1 1194 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β π β πΈ) |
8 | | lincext.e |
. . . . . . . 8
β’ πΈ = (Baseβπ
) |
9 | | lincext.n |
. . . . . . . 8
β’ π = (invgβπ
) |
10 | 8, 9 | grpinvcl 18874 |
. . . . . . 7
β’ ((π
β Grp β§ π β πΈ) β (πβπ) β πΈ) |
11 | 6, 7, 10 | syl2anc 584 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (πβπ) β πΈ) |
12 | 11 | ad2antrr 724 |
. . . . 5
β’
(((((π β LMod
β§ π β π«
π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β§ π§ β π) β§ π§ = π) β (πβπ) β πΈ) |
13 | | elmapi 8845 |
. . . . . . . . 9
β’ (πΊ β (πΈ βm (π β {π})) β πΊ:(π β {π})βΆπΈ) |
14 | | df-ne 2941 |
. . . . . . . . . . . . . 14
β’ (π§ β π β Β¬ π§ = π) |
15 | 14 | biimpri 227 |
. . . . . . . . . . . . 13
β’ (Β¬
π§ = π β π§ β π) |
16 | 15 | anim2i 617 |
. . . . . . . . . . . 12
β’ ((π§ β π β§ Β¬ π§ = π) β (π§ β π β§ π§ β π)) |
17 | | eldifsn 4790 |
. . . . . . . . . . . 12
β’ (π§ β (π β {π}) β (π§ β π β§ π§ β π)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π§ β π β§ Β¬ π§ = π) β π§ β (π β {π})) |
19 | | ffvelcdm 7083 |
. . . . . . . . . . 11
β’ ((πΊ:(π β {π})βΆπΈ β§ π§ β (π β {π})) β (πΊβπ§) β πΈ) |
20 | 18, 19 | sylan2 593 |
. . . . . . . . . 10
β’ ((πΊ:(π β {π})βΆπΈ β§ (π§ β π β§ Β¬ π§ = π)) β (πΊβπ§) β πΈ) |
21 | 20 | ex 413 |
. . . . . . . . 9
β’ (πΊ:(π β {π})βΆπΈ β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
22 | 13, 21 | syl 17 |
. . . . . . . 8
β’ (πΊ β (πΈ βm (π β {π})) β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
23 | 22 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π}))) β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
24 | 23 | adantl 482 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β ((π§ β π β§ Β¬ π§ = π) β (πΊβπ§) β πΈ)) |
25 | 24 | impl 456 |
. . . . 5
β’
(((((π β LMod
β§ π β π«
π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β§ π§ β π) β§ Β¬ π§ = π) β (πΊβπ§) β πΈ) |
26 | 12, 25 | ifclda 4563 |
. . . 4
β’ ((((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β§ π§ β π) β if(π§ = π, (πβπ), (πΊβπ§)) β πΈ) |
27 | 26 | fmpttd 7116 |
. . 3
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))):πβΆπΈ) |
28 | | simpr 485 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅) β π β π« π΅) |
29 | 8 | fvexi 6905 |
. . . . . 6
β’ πΈ β V |
30 | 28, 29 | jctil 520 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅) β (πΈ β V β§ π β π« π΅)) |
31 | 30 | adantr 481 |
. . . 4
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (πΈ β V β§ π β π« π΅)) |
32 | | elmapg 8835 |
. . . 4
β’ ((πΈ β V β§ π β π« π΅) β ((π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β (πΈ βm π) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))):πβΆπΈ)) |
33 | 31, 32 | syl 17 |
. . 3
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β ((π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β (πΈ βm π) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))):πβΆπΈ)) |
34 | 27, 33 | mpbird 256 |
. 2
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β (π§ β π β¦ if(π§ = π, (πβπ), (πΊβπ§))) β (πΈ βm π)) |
35 | 1, 34 | eqeltrid 2837 |
1
β’ (((π β LMod β§ π β π« π΅) β§ (π β πΈ β§ π β π β§ πΊ β (πΈ βm (π β {π})))) β πΉ β (πΈ βm π)) |