Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7424 |
. . . . . . . 8
β’ (πΌ = β
β
(Baseβ(πΌ Mat π
)) = (Baseβ(β
Mat
π
))) |
2 | | mat0dimbas0 22290 |
. . . . . . . 8
β’ (π
β Field β
(Baseβ(β
Mat π
)) = {β
}) |
3 | 1, 2 | sylan9eq 2784 |
. . . . . . 7
β’ ((πΌ = β
β§ π
β Field) β
(Baseβ(πΌ Mat π
)) = {β
}) |
4 | 3 | eleq2d 2811 |
. . . . . 6
β’ ((πΌ = β
β§ π
β Field) β (π β (Baseβ(πΌ Mat π
)) β π β {β
})) |
5 | | elsni 4637 |
. . . . . 6
β’ (π β {β
} β π = β
) |
6 | 4, 5 | syl6bi 253 |
. . . . 5
β’ ((πΌ = β
β§ π
β Field) β (π β (Baseβ(πΌ Mat π
)) β π = β
)) |
7 | 6 | imdistanda 571 |
. . . 4
β’ (πΌ = β
β ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (π
β Field β§ π = β
))) |
8 | 7 | impcom 407 |
. . 3
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ = β
) β (π
β Field β§ π = β
)) |
9 | | isfld 20588 |
. . . . . . . 8
β’ (π
β Field β (π
β DivRing β§ π
β CRing)) |
10 | 9 | simplbi 497 |
. . . . . . 7
β’ (π
β Field β π
β
DivRing) |
11 | | drngring 20584 |
. . . . . . 7
β’ (π
β DivRing β π
β Ring) |
12 | | eqid 2724 |
. . . . . . . . 9
β’ (β
Mat π
) = (β
Mat π
) |
13 | 12 | mat0dimid 22292 |
. . . . . . . 8
β’ (π
β Ring β
(1rβ(β
Mat π
)) = β
) |
14 | | 0fin 9167 |
. . . . . . . . . 10
β’ β
β Fin |
15 | 12 | matring 22267 |
. . . . . . . . . 10
β’ ((β
β Fin β§ π
β
Ring) β (β
Mat π
) β Ring) |
16 | 14, 15 | mpan 687 |
. . . . . . . . 9
β’ (π
β Ring β (β
Mat
π
) β
Ring) |
17 | | eqid 2724 |
. . . . . . . . . 10
β’
(Unitβ(β
Mat π
)) = (Unitβ(β
Mat π
)) |
18 | | eqid 2724 |
. . . . . . . . . 10
β’
(1rβ(β
Mat π
)) = (1rβ(β
Mat π
)) |
19 | 17, 18 | 1unit 20266 |
. . . . . . . . 9
β’ ((β
Mat π
) β Ring β
(1rβ(β
Mat π
)) β (Unitβ(β
Mat π
))) |
20 | 16, 19 | syl 17 |
. . . . . . . 8
β’ (π
β Ring β
(1rβ(β
Mat π
)) β (Unitβ(β
Mat π
))) |
21 | 13, 20 | eqeltrrd 2826 |
. . . . . . 7
β’ (π
β Ring β β
β (Unitβ(β
Mat π
))) |
22 | 10, 11, 21 | 3syl 18 |
. . . . . 6
β’ (π
β Field β β
β (Unitβ(β
Mat π
))) |
23 | | f0 6762 |
. . . . . . . . 9
β’
β
:β
βΆ(Baseβ(π
freeLMod β
)) |
24 | | dm0 5910 |
. . . . . . . . . 10
β’ dom
β
= β
|
25 | 24 | feq2i 6699 |
. . . . . . . . 9
β’
(β
:dom β
βΆ(Baseβ(π
freeLMod β
)) β
β
:β
βΆ(Baseβ(π
freeLMod β
))) |
26 | 23, 25 | mpbir 230 |
. . . . . . . 8
β’
β
:dom β
βΆ(Baseβ(π
freeLMod β
)) |
27 | | rzal 4500 |
. . . . . . . . 9
β’ (dom
β
= β
β βπ₯ β dom β
βπ¦ β ((Baseβ(Scalarβ(π
freeLMod β
))) β
{(0gβ(Scalarβ(π
freeLMod β
)))}) Β¬ (π¦(
Β·π β(π
freeLMod β
))(β
βπ₯)) β ((LSpanβ(π
freeLMod
β
))β(β
β (dom β
β {π₯})))) |
28 | 24, 27 | ax-mp 5 |
. . . . . . . 8
β’
βπ₯ β dom
β
βπ¦ β
((Baseβ(Scalarβ(π
freeLMod β
))) β
{(0gβ(Scalarβ(π
freeLMod β
)))}) Β¬ (π¦(
Β·π β(π
freeLMod β
))(β
βπ₯)) β ((LSpanβ(π
freeLMod
β
))β(β
β (dom β
β {π₯}))) |
29 | | ovex 7434 |
. . . . . . . . 9
β’ (π
freeLMod β
) β
V |
30 | | eqid 2724 |
. . . . . . . . . 10
β’
(Baseβ(π
freeLMod β
)) = (Baseβ(π
freeLMod β
)) |
31 | | eqid 2724 |
. . . . . . . . . 10
β’ (
Β·π β(π
freeLMod β
)) = (
Β·π β(π
freeLMod β
)) |
32 | | eqid 2724 |
. . . . . . . . . 10
β’
(LSpanβ(π
freeLMod β
)) = (LSpanβ(π
freeLMod β
)) |
33 | | eqid 2724 |
. . . . . . . . . 10
β’
(Scalarβ(π
freeLMod β
)) = (Scalarβ(π
freeLMod β
)) |
34 | | eqid 2724 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβ(π
freeLMod β
))) =
(Baseβ(Scalarβ(π
freeLMod β
))) |
35 | | eqid 2724 |
. . . . . . . . . 10
β’
(0gβ(Scalarβ(π
freeLMod β
))) =
(0gβ(Scalarβ(π
freeLMod β
))) |
36 | 30, 31, 32, 33, 34, 35 | islindf 21675 |
. . . . . . . . 9
β’ (((π
freeLMod β
) β V
β§ β
β Fin) β (β
LIndF (π
freeLMod β
) β (β
:dom
β
βΆ(Baseβ(π
freeLMod β
)) β§ βπ₯ β dom β
βπ¦ β
((Baseβ(Scalarβ(π
freeLMod β
))) β
{(0gβ(Scalarβ(π
freeLMod β
)))}) Β¬ (π¦(
Β·π β(π
freeLMod β
))(β
βπ₯)) β ((LSpanβ(π
freeLMod
β
))β(β
β (dom β
β {π₯})))))) |
37 | 29, 14, 36 | mp2an 689 |
. . . . . . . 8
β’ (β
LIndF (π
freeLMod β
)
β (β
:dom β
βΆ(Baseβ(π
freeLMod β
)) β§ βπ₯ β dom β
βπ¦ β
((Baseβ(Scalarβ(π
freeLMod β
))) β
{(0gβ(Scalarβ(π
freeLMod β
)))}) Β¬ (π¦(
Β·π β(π
freeLMod β
))(β
βπ₯)) β ((LSpanβ(π
freeLMod
β
))β(β
β (dom β
β {π₯}))))) |
38 | 26, 28, 37 | mpbir2an 708 |
. . . . . . 7
β’ β
LIndF (π
freeLMod
β
) |
39 | 38 | a1i 11 |
. . . . . 6
β’ (π
β Field β β
LIndF (π
freeLMod
β
)) |
40 | 22, 39 | 2thd 265 |
. . . . 5
β’ (π
β Field β (β
β (Unitβ(β
Mat π
)) β β
LIndF (π
freeLMod β
))) |
41 | | fvoveq1 7424 |
. . . . . . . 8
β’ (πΌ = β
β
(Unitβ(πΌ Mat π
)) = (Unitβ(β
Mat
π
))) |
42 | | eleq12 2815 |
. . . . . . . 8
β’ ((π = β
β§
(Unitβ(πΌ Mat π
)) = (Unitβ(β
Mat
π
))) β (π β (Unitβ(πΌ Mat π
)) β β
β
(Unitβ(β
Mat π
)))) |
43 | 41, 42 | sylan2 592 |
. . . . . . 7
β’ ((π = β
β§ πΌ = β
) β (π β (Unitβ(πΌ Mat π
)) β β
β
(Unitβ(β
Mat π
)))) |
44 | | cureq 36954 |
. . . . . . . . 9
β’ (π = β
β curry π = curry
β
) |
45 | | df-cur 8247 |
. . . . . . . . . 10
β’ curry
β
= (π₯ β dom dom
β
β¦ {β¨π¦,
π§β© β£ β¨π₯, π¦β©β
π§}) |
46 | 24 | dmeqi 5894 |
. . . . . . . . . . . 12
β’ dom dom
β
= dom β
|
47 | 46, 24 | eqtri 2752 |
. . . . . . . . . . 11
β’ dom dom
β
= β
|
48 | | mpteq1 5231 |
. . . . . . . . . . 11
β’ (dom dom
β
= β
β (π₯
β dom dom β
β¦ {β¨π¦, π§β© β£ β¨π₯, π¦β©β
π§}) = (π₯ β β
β¦ {β¨π¦, π§β© β£ β¨π₯, π¦β©β
π§})) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
β’ (π₯ β dom dom β
β¦
{β¨π¦, π§β© β£ β¨π₯, π¦β©β
π§}) = (π₯ β β
β¦ {β¨π¦, π§β© β£ β¨π₯, π¦β©β
π§}) |
50 | | mpt0 6682 |
. . . . . . . . . 10
β’ (π₯ β β
β¦
{β¨π¦, π§β© β£ β¨π₯, π¦β©β
π§}) = β
|
51 | 45, 49, 50 | 3eqtri 2756 |
. . . . . . . . 9
β’ curry
β
= β
|
52 | 44, 51 | eqtrdi 2780 |
. . . . . . . 8
β’ (π = β
β curry π = β
) |
53 | | oveq2 7409 |
. . . . . . . 8
β’ (πΌ = β
β (π
freeLMod πΌ) = (π
freeLMod β
)) |
54 | 52, 53 | breqan12d 5154 |
. . . . . . 7
β’ ((π = β
β§ πΌ = β
) β (curry π LIndF (π
freeLMod πΌ) β β
LIndF (π
freeLMod β
))) |
55 | 43, 54 | bibi12d 345 |
. . . . . 6
β’ ((π = β
β§ πΌ = β
) β ((π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ)) β (β
β
(Unitβ(β
Mat π
)) β β
LIndF (π
freeLMod β
)))) |
56 | 55 | biimparc 479 |
. . . . 5
β’
(((β
β (Unitβ(β
Mat π
)) β β
LIndF (π
freeLMod β
)) β§ (π = β
β§ πΌ = β
)) β (π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ))) |
57 | 40, 56 | sylan 579 |
. . . 4
β’ ((π
β Field β§ (π = β
β§ πΌ = β
)) β (π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ))) |
58 | 57 | anassrs 467 |
. . 3
β’ (((π
β Field β§ π = β
) β§ πΌ = β
) β (π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ))) |
59 | 8, 58 | sylancom 587 |
. 2
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ = β
) β (π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ))) |
60 | 9 | simprbi 496 |
. . . . 5
β’ (π
β Field β π
β CRing) |
61 | | eqid 2724 |
. . . . . 6
β’ (πΌ Mat π
) = (πΌ Mat π
) |
62 | | eqid 2724 |
. . . . . 6
β’ (πΌ maDet π
) = (πΌ maDet π
) |
63 | | eqid 2724 |
. . . . . 6
β’
(Baseβ(πΌ Mat
π
)) = (Baseβ(πΌ Mat π
)) |
64 | | eqid 2724 |
. . . . . 6
β’
(Unitβ(πΌ Mat
π
)) = (Unitβ(πΌ Mat π
)) |
65 | | eqid 2724 |
. . . . . 6
β’
(Unitβπ
) =
(Unitβπ
) |
66 | 61, 62, 63, 64, 65 | matunit 22502 |
. . . . 5
β’ ((π
β CRing β§ π β (Baseβ(πΌ Mat π
))) β (π β (Unitβ(πΌ Mat π
)) β ((πΌ maDet π
)βπ) β (Unitβπ
))) |
67 | 60, 66 | sylan 579 |
. . . 4
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (π β (Unitβ(πΌ Mat π
)) β ((πΌ maDet π
)βπ) β (Unitβπ
))) |
68 | 67 | adantr 480 |
. . 3
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (π β (Unitβ(πΌ Mat π
)) β ((πΌ maDet π
)βπ) β (Unitβπ
))) |
69 | | eqid 2724 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
70 | | eqid 2724 |
. . . . . . . . . 10
β’
(0gβπ
) = (0gβπ
) |
71 | 69, 65, 70 | drngunit 20582 |
. . . . . . . . 9
β’ (π
β DivRing β (((πΌ maDet π
)βπ) β (Unitβπ
) β (((πΌ maDet π
)βπ) β (Baseβπ
) β§ ((πΌ maDet π
)βπ) β (0gβπ
)))) |
72 | 10, 71 | syl 17 |
. . . . . . . 8
β’ (π
β Field β (((πΌ maDet π
)βπ) β (Unitβπ
) β (((πΌ maDet π
)βπ) β (Baseβπ
) β§ ((πΌ maDet π
)βπ) β (0gβπ
)))) |
73 | 72 | adantr 480 |
. . . . . . 7
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (((πΌ maDet π
)βπ) β (Unitβπ
) β (((πΌ maDet π
)βπ) β (Baseβπ
) β§ ((πΌ maDet π
)βπ) β (0gβπ
)))) |
74 | 62, 61, 63, 69 | mdetcl 22420 |
. . . . . . . . 9
β’ ((π
β CRing β§ π β (Baseβ(πΌ Mat π
))) β ((πΌ maDet π
)βπ) β (Baseβπ
)) |
75 | 60, 74 | sylan 579 |
. . . . . . . 8
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β ((πΌ maDet π
)βπ) β (Baseβπ
)) |
76 | 75 | biantrurd 532 |
. . . . . . 7
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (((πΌ maDet π
)βπ) β (0gβπ
) β (((πΌ maDet π
)βπ) β (Baseβπ
) β§ ((πΌ maDet π
)βπ) β (0gβπ
)))) |
77 | 73, 76 | bitr4d 282 |
. . . . . 6
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (((πΌ maDet π
)βπ) β (Unitβπ
) β ((πΌ maDet π
)βπ) β (0gβπ
))) |
78 | 77 | adantr 480 |
. . . . 5
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (((πΌ maDet π
)βπ) β (Unitβπ
) β ((πΌ maDet π
)βπ) β (0gβπ
))) |
79 | 61, 63 | matrcl 22234 |
. . . . . . . . . . . 12
β’ (π β (Baseβ(πΌ Mat π
)) β (πΌ β Fin β§ π
β V)) |
80 | 79 | simpld 494 |
. . . . . . . . . . 11
β’ (π β (Baseβ(πΌ Mat π
)) β πΌ β Fin) |
81 | 80 | pm4.71i 559 |
. . . . . . . . . 10
β’ (π β (Baseβ(πΌ Mat π
)) β (π β (Baseβ(πΌ Mat π
)) β§ πΌ β Fin)) |
82 | | xpfi 9313 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ β Fin β§ πΌ β Fin) β (πΌ Γ πΌ) β Fin) |
83 | 82 | anidms 566 |
. . . . . . . . . . . . . . . 16
β’ (πΌ β Fin β (πΌ Γ πΌ) β Fin) |
84 | | eqid 2724 |
. . . . . . . . . . . . . . . . 17
β’ (π
freeLMod (πΌ Γ πΌ)) = (π
freeLMod (πΌ Γ πΌ)) |
85 | 84, 69 | frlmfibas 21625 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Field β§ (πΌ Γ πΌ) β Fin) β ((Baseβπ
) βm (πΌ Γ πΌ)) = (Baseβ(π
freeLMod (πΌ Γ πΌ)))) |
86 | 83, 85 | sylan2 592 |
. . . . . . . . . . . . . . 15
β’ ((π
β Field β§ πΌ β Fin) β
((Baseβπ
)
βm (πΌ
Γ πΌ)) =
(Baseβ(π
freeLMod
(πΌ Γ πΌ)))) |
87 | 61, 84 | matbas 22235 |
. . . . . . . . . . . . . . . 16
β’ ((πΌ β Fin β§ π
β Field) β
(Baseβ(π
freeLMod
(πΌ Γ πΌ))) = (Baseβ(πΌ Mat π
))) |
88 | 87 | ancoms 458 |
. . . . . . . . . . . . . . 15
β’ ((π
β Field β§ πΌ β Fin) β
(Baseβ(π
freeLMod
(πΌ Γ πΌ))) = (Baseβ(πΌ Mat π
))) |
89 | 86, 88 | eqtrd 2764 |
. . . . . . . . . . . . . 14
β’ ((π
β Field β§ πΌ β Fin) β
((Baseβπ
)
βm (πΌ
Γ πΌ)) =
(Baseβ(πΌ Mat π
))) |
90 | 89 | eleq2d 2811 |
. . . . . . . . . . . . 13
β’ ((π
β Field β§ πΌ β Fin) β (π β ((Baseβπ
) βm (πΌ Γ πΌ)) β π β (Baseβ(πΌ Mat π
)))) |
91 | | fvex 6894 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ
)
β V |
92 | | elmapg 8829 |
. . . . . . . . . . . . . . 15
β’
(((Baseβπ
)
β V β§ (πΌ Γ
πΌ) β Fin) β
(π β
((Baseβπ
)
βm (πΌ
Γ πΌ)) β π:(πΌ Γ πΌ)βΆ(Baseβπ
))) |
93 | 91, 83, 92 | sylancr 586 |
. . . . . . . . . . . . . 14
β’ (πΌ β Fin β (π β ((Baseβπ
) βm (πΌ Γ πΌ)) β π:(πΌ Γ πΌ)βΆ(Baseβπ
))) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . 13
β’ ((π
β Field β§ πΌ β Fin) β (π β ((Baseβπ
) βm (πΌ Γ πΌ)) β π:(πΌ Γ πΌ)βΆ(Baseβπ
))) |
95 | 90, 94 | bitr3d 281 |
. . . . . . . . . . . 12
β’ ((π
β Field β§ πΌ β Fin) β (π β (Baseβ(πΌ Mat π
)) β π:(πΌ Γ πΌ)βΆ(Baseβπ
))) |
96 | 95 | ex 412 |
. . . . . . . . . . 11
β’ (π
β Field β (πΌ β Fin β (π β (Baseβ(πΌ Mat π
)) β π:(πΌ Γ πΌ)βΆ(Baseβπ
)))) |
97 | 96 | pm5.32rd 577 |
. . . . . . . . . 10
β’ (π
β Field β ((π β (Baseβ(πΌ Mat π
)) β§ πΌ β Fin) β (π:(πΌ Γ πΌ)βΆ(Baseβπ
) β§ πΌ β Fin))) |
98 | 81, 97 | bitrid 283 |
. . . . . . . . 9
β’ (π
β Field β (π β (Baseβ(πΌ Mat π
)) β (π:(πΌ Γ πΌ)βΆ(Baseβπ
) β§ πΌ β Fin))) |
99 | 98 | biimpd 228 |
. . . . . . . 8
β’ (π
β Field β (π β (Baseβ(πΌ Mat π
)) β (π:(πΌ Γ πΌ)βΆ(Baseβπ
) β§ πΌ β Fin))) |
100 | 99 | imdistani 568 |
. . . . . . 7
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (π
β Field β§ (π:(πΌ Γ πΌ)βΆ(Baseβπ
) β§ πΌ β Fin))) |
101 | | anass 468 |
. . . . . . 7
β’ (((π
β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ
)) β§ πΌ β Fin) β (π
β Field β§ (π:(πΌ Γ πΌ)βΆ(Baseβπ
) β§ πΌ β Fin))) |
102 | 100, 101 | sylibr 233 |
. . . . . 6
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β ((π
β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ
)) β§ πΌ β Fin)) |
103 | | eldifsn 4782 |
. . . . . . . 8
β’ (πΌ β (Fin β {β
})
β (πΌ β Fin β§
πΌ β
β
)) |
104 | | matunitlindflem1 36974 |
. . . . . . . . 9
β’ (((π
β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ
)) β§ πΌ β (Fin β {β
})) β
(Β¬ curry π LIndF (π
freeLMod πΌ) β ((πΌ maDet π
)βπ) = (0gβπ
))) |
105 | 104 | necon1ad 2949 |
. . . . . . . 8
β’ (((π
β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ
)) β§ πΌ β (Fin β {β
})) β
(((πΌ maDet π
)βπ) β (0gβπ
) β curry π LIndF (π
freeLMod πΌ))) |
106 | 103, 105 | sylan2br 594 |
. . . . . . 7
β’ (((π
β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ
)) β§ (πΌ β Fin β§ πΌ β β
)) β (((πΌ maDet π
)βπ) β (0gβπ
) β curry π LIndF (π
freeLMod πΌ))) |
107 | 106 | anassrs 467 |
. . . . . 6
β’ ((((π
β Field β§ π:(πΌ Γ πΌ)βΆ(Baseβπ
)) β§ πΌ β Fin) β§ πΌ β β
) β (((πΌ maDet π
)βπ) β (0gβπ
) β curry π LIndF (π
freeLMod πΌ))) |
108 | 102, 107 | sylan 579 |
. . . . 5
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (((πΌ maDet π
)βπ) β (0gβπ
) β curry π LIndF (π
freeLMod πΌ))) |
109 | 78, 108 | sylbid 239 |
. . . 4
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (((πΌ maDet π
)βπ) β (Unitβπ
) β curry π LIndF (π
freeLMod πΌ))) |
110 | | matunitlindflem2 36975 |
. . . . 5
β’ ((((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β§ curry π LIndF (π
freeLMod πΌ)) β ((πΌ maDet π
)βπ) β (Unitβπ
)) |
111 | 110 | ex 412 |
. . . 4
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (curry π LIndF (π
freeLMod πΌ) β ((πΌ maDet π
)βπ) β (Unitβπ
))) |
112 | 109, 111 | impbid 211 |
. . 3
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (((πΌ maDet π
)βπ) β (Unitβπ
) β curry π LIndF (π
freeLMod πΌ))) |
113 | 68, 112 | bitrd 279 |
. 2
β’ (((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β§ πΌ β β
) β (π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ))) |
114 | 59, 113 | pm2.61dane 3021 |
1
β’ ((π
β Field β§ π β (Baseβ(πΌ Mat π
))) β (π β (Unitβ(πΌ Mat π
)) β curry π LIndF (π
freeLMod πΌ))) |