Step | Hyp | Ref
| Expression |
1 | | nne 2945 |
. . . . . . 7
β’ (Β¬
(πΊβπ§) β 0 β (πΊβπ§) = 0 ) |
2 | 1 | ralbii 3094 |
. . . . . 6
β’
(βπ§ β
π Β¬ (πΊβπ§) β 0 β βπ§ β π (πΊβπ§) = 0 ) |
3 | | lfl1.d |
. . . . . . . . . 10
β’ π· = (Scalarβπ) |
4 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ·) =
(Baseβπ·) |
5 | | lfl1.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
6 | | lfl1.f |
. . . . . . . . . 10
β’ πΉ = (LFnlβπ) |
7 | 3, 4, 5, 6 | lflf 37933 |
. . . . . . . . 9
β’ ((π β LVec β§ πΊ β πΉ) β πΊ:πβΆ(Baseβπ·)) |
8 | 7 | ffnd 6719 |
. . . . . . . 8
β’ ((π β LVec β§ πΊ β πΉ) β πΊ Fn π) |
9 | | fconstfv 7214 |
. . . . . . . . 9
β’ (πΊ:πβΆ{ 0 } β (πΊ Fn π β§ βπ§ β π (πΊβπ§) = 0 )) |
10 | 9 | simplbi2 502 |
. . . . . . . 8
β’ (πΊ Fn π β (βπ§ β π (πΊβπ§) = 0 β πΊ:πβΆ{ 0 })) |
11 | 8, 10 | syl 17 |
. . . . . . 7
β’ ((π β LVec β§ πΊ β πΉ) β (βπ§ β π (πΊβπ§) = 0 β πΊ:πβΆ{ 0 })) |
12 | | lfl1.o |
. . . . . . . . 9
β’ 0 =
(0gβπ·) |
13 | 12 | fvexi 6906 |
. . . . . . . 8
β’ 0 β
V |
14 | 13 | fconst2 7206 |
. . . . . . 7
β’ (πΊ:πβΆ{ 0 } β πΊ = (π Γ { 0 })) |
15 | 11, 14 | imbitrdi 250 |
. . . . . 6
β’ ((π β LVec β§ πΊ β πΉ) β (βπ§ β π (πΊβπ§) = 0 β πΊ = (π Γ { 0 }))) |
16 | 2, 15 | biimtrid 241 |
. . . . 5
β’ ((π β LVec β§ πΊ β πΉ) β (βπ§ β π Β¬ (πΊβπ§) β 0 β πΊ = (π Γ { 0 }))) |
17 | 16 | necon3ad 2954 |
. . . 4
β’ ((π β LVec β§ πΊ β πΉ) β (πΊ β (π Γ { 0 }) β Β¬
βπ§ β π Β¬ (πΊβπ§) β 0 )) |
18 | | dfrex2 3074 |
. . . 4
β’
(βπ§ β
π (πΊβπ§) β 0 β Β¬ βπ§ β π Β¬ (πΊβπ§) β 0 ) |
19 | 17, 18 | syl6ibr 252 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ) β (πΊ β (π Γ { 0 }) β βπ§ β π (πΊβπ§) β 0 )) |
20 | 19 | 3impia 1118 |
. 2
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β βπ§ β π (πΊβπ§) β 0 ) |
21 | | simp1l 1198 |
. . . . . . 7
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β π β LVec) |
22 | | lveclmod 20717 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β π β LMod) |
24 | 3 | lvecdrng 20716 |
. . . . . . . 8
β’ (π β LVec β π· β
DivRing) |
25 | 21, 24 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β π· β DivRing) |
26 | | simp1r 1199 |
. . . . . . . 8
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β πΊ β πΉ) |
27 | | simp2 1138 |
. . . . . . . 8
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β π§ β π) |
28 | 3, 4, 5, 6 | lflcl 37934 |
. . . . . . . 8
β’ ((π β LVec β§ πΊ β πΉ β§ π§ β π) β (πΊβπ§) β (Baseβπ·)) |
29 | 21, 26, 27, 28 | syl3anc 1372 |
. . . . . . 7
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β (πΊβπ§) β (Baseβπ·)) |
30 | | simp3 1139 |
. . . . . . 7
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β (πΊβπ§) β 0 ) |
31 | | eqid 2733 |
. . . . . . . 8
β’
(invrβπ·) = (invrβπ·) |
32 | 4, 12, 31 | drnginvrcl 20379 |
. . . . . . 7
β’ ((π· β DivRing β§ (πΊβπ§) β (Baseβπ·) β§ (πΊβπ§) β 0 ) β
((invrβπ·)β(πΊβπ§)) β (Baseβπ·)) |
33 | 25, 29, 30, 32 | syl3anc 1372 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β
((invrβπ·)β(πΊβπ§)) β (Baseβπ·)) |
34 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
35 | 5, 3, 34, 4 | lmodvscl 20489 |
. . . . . 6
β’ ((π β LMod β§
((invrβπ·)β(πΊβπ§)) β (Baseβπ·) β§ π§ β π) β (((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§) β π) |
36 | 23, 33, 27, 35 | syl3anc 1372 |
. . . . 5
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β
(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§) β π) |
37 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπ·) = (.rβπ·) |
38 | 3, 4, 37, 5, 34, 6 | lflmul 37938 |
. . . . . . 7
β’ ((π β LMod β§ πΊ β πΉ β§ (((invrβπ·)β(πΊβπ§)) β (Baseβπ·) β§ π§ β π)) β (πΊβ(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§)) = (((invrβπ·)β(πΊβπ§))(.rβπ·)(πΊβπ§))) |
39 | 23, 26, 33, 27, 38 | syl112anc 1375 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β (πΊβ(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§)) = (((invrβπ·)β(πΊβπ§))(.rβπ·)(πΊβπ§))) |
40 | | lfl1.u |
. . . . . . . 8
β’ 1 =
(1rβπ·) |
41 | 4, 12, 37, 40, 31 | drnginvrl 20382 |
. . . . . . 7
β’ ((π· β DivRing β§ (πΊβπ§) β (Baseβπ·) β§ (πΊβπ§) β 0 ) β
(((invrβπ·)β(πΊβπ§))(.rβπ·)(πΊβπ§)) = 1 ) |
42 | 25, 29, 30, 41 | syl3anc 1372 |
. . . . . 6
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β
(((invrβπ·)β(πΊβπ§))(.rβπ·)(πΊβπ§)) = 1 ) |
43 | 39, 42 | eqtrd 2773 |
. . . . 5
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β (πΊβ(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§)) = 1 ) |
44 | | fveqeq2 6901 |
. . . . . 6
β’ (π₯ =
(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§) β ((πΊβπ₯) = 1 β (πΊβ(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§)) = 1 )) |
45 | 44 | rspcev 3613 |
. . . . 5
β’
(((((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§) β π β§ (πΊβ(((invrβπ·)β(πΊβπ§))( Β·π
βπ)π§)) = 1 ) β βπ₯ β π (πΊβπ₯) = 1 ) |
46 | 36, 43, 45 | syl2anc 585 |
. . . 4
β’ (((π β LVec β§ πΊ β πΉ) β§ π§ β π β§ (πΊβπ§) β 0 ) β βπ₯ β π (πΊβπ₯) = 1 ) |
47 | 46 | rexlimdv3a 3160 |
. . 3
β’ ((π β LVec β§ πΊ β πΉ) β (βπ§ β π (πΊβπ§) β 0 β βπ₯ β π (πΊβπ₯) = 1 )) |
48 | 47 | 3adant3 1133 |
. 2
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β (βπ§ β π (πΊβπ§) β 0 β βπ₯ β π (πΊβπ₯) = 1 )) |
49 | 20, 48 | mpd 15 |
1
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β βπ₯ β π (πΊβπ₯) = 1 ) |