Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝐼 = ∅ → (𝐼 Mat 𝑅) = (∅ Mat 𝑅)) |
2 | 1 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝐼 = ∅ →
(Base‘(𝐼 Mat 𝑅)) = (Base‘(∅ Mat
𝑅))) |
3 | | mat0dimbas0 20091 |
. . . . . . . 8
⊢ (𝑅 ∈ Field →
(Base‘(∅ Mat 𝑅)) = {∅}) |
4 | 2, 3 | sylan9eq 2664 |
. . . . . . 7
⊢ ((𝐼 = ∅ ∧ 𝑅 ∈ Field) →
(Base‘(𝐼 Mat 𝑅)) = {∅}) |
5 | 4 | eleq2d 2673 |
. . . . . 6
⊢ ((𝐼 = ∅ ∧ 𝑅 ∈ Field) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀 ∈ {∅})) |
6 | | elsni 4142 |
. . . . . 6
⊢ (𝑀 ∈ {∅} → 𝑀 = ∅) |
7 | 5, 6 | syl6bi 242 |
. . . . 5
⊢ ((𝐼 = ∅ ∧ 𝑅 ∈ Field) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝑀 = ∅)) |
8 | 7 | imdistanda 725 |
. . . 4
⊢ (𝐼 = ∅ → ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Field ∧ 𝑀 = ∅))) |
9 | 8 | impcom 445 |
. . 3
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 = ∅) → (𝑅 ∈ Field ∧ 𝑀 = ∅)) |
10 | | isfld 18579 |
. . . . . . . 8
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
11 | 10 | simplbi 475 |
. . . . . . 7
⊢ (𝑅 ∈ Field → 𝑅 ∈
DivRing) |
12 | | drngring 18577 |
. . . . . . 7
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢ (∅
Mat 𝑅) = (∅ Mat 𝑅) |
14 | 13 | mat0dimid 20093 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘(∅ Mat 𝑅)) = ∅) |
15 | | 0fin 8073 |
. . . . . . . . . 10
⊢ ∅
∈ Fin |
16 | 13 | matring 20068 |
. . . . . . . . . 10
⊢ ((∅
∈ Fin ∧ 𝑅 ∈
Ring) → (∅ Mat 𝑅) ∈ Ring) |
17 | 15, 16 | mpan 702 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (∅ Mat
𝑅) ∈
Ring) |
18 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Unit‘(∅ Mat 𝑅)) = (Unit‘(∅ Mat 𝑅)) |
19 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1r‘(∅ Mat 𝑅)) = (1r‘(∅ Mat 𝑅)) |
20 | 18, 19 | 1unit 18481 |
. . . . . . . . 9
⊢ ((∅
Mat 𝑅) ∈ Ring →
(1r‘(∅ Mat 𝑅)) ∈ (Unit‘(∅ Mat 𝑅))) |
21 | 17, 20 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘(∅ Mat 𝑅)) ∈ (Unit‘(∅ Mat 𝑅))) |
22 | 14, 21 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ∅
∈ (Unit‘(∅ Mat 𝑅))) |
23 | 11, 12, 22 | 3syl 18 |
. . . . . 6
⊢ (𝑅 ∈ Field → ∅
∈ (Unit‘(∅ Mat 𝑅))) |
24 | | f0 5999 |
. . . . . . . . 9
⊢
∅:∅⟶(Base‘(𝑅 freeLMod ∅)) |
25 | | dm0 5260 |
. . . . . . . . . 10
⊢ dom
∅ = ∅ |
26 | 25 | feq2i 5950 |
. . . . . . . . 9
⊢
(∅:dom ∅⟶(Base‘(𝑅 freeLMod ∅)) ↔
∅:∅⟶(Base‘(𝑅 freeLMod ∅))) |
27 | 24, 26 | mpbir 220 |
. . . . . . . 8
⊢
∅:dom ∅⟶(Base‘(𝑅 freeLMod ∅)) |
28 | | rzal 4025 |
. . . . . . . . 9
⊢ (dom
∅ = ∅ → ∀𝑥 ∈ dom ∅∀𝑦 ∈ ((Base‘(Scalar‘(𝑅 freeLMod ∅))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod ∅)))}) ¬ (𝑦(
·𝑠 ‘(𝑅 freeLMod ∅))(∅‘𝑥)) ∈ ((LSpan‘(𝑅 freeLMod
∅))‘(∅ “ (dom ∅ ∖ {𝑥})))) |
29 | 25, 28 | ax-mp 5 |
. . . . . . . 8
⊢
∀𝑥 ∈ dom
∅∀𝑦 ∈
((Base‘(Scalar‘(𝑅 freeLMod ∅))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod ∅)))}) ¬ (𝑦(
·𝑠 ‘(𝑅 freeLMod ∅))(∅‘𝑥)) ∈ ((LSpan‘(𝑅 freeLMod
∅))‘(∅ “ (dom ∅ ∖ {𝑥}))) |
30 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑅 freeLMod ∅) ∈
V |
31 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(𝑅
freeLMod ∅)) = (Base‘(𝑅 freeLMod ∅)) |
32 | | eqid 2610 |
. . . . . . . . . 10
⊢ (
·𝑠 ‘(𝑅 freeLMod ∅)) = (
·𝑠 ‘(𝑅 freeLMod ∅)) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢
(LSpan‘(𝑅
freeLMod ∅)) = (LSpan‘(𝑅 freeLMod ∅)) |
34 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Scalar‘(𝑅
freeLMod ∅)) = (Scalar‘(𝑅 freeLMod ∅)) |
35 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘(𝑅 freeLMod ∅))) =
(Base‘(Scalar‘(𝑅 freeLMod ∅))) |
36 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘(𝑅 freeLMod ∅))) =
(0g‘(Scalar‘(𝑅 freeLMod ∅))) |
37 | 31, 32, 33, 34, 35, 36 | islindf 19970 |
. . . . . . . . 9
⊢ (((𝑅 freeLMod ∅) ∈ V
∧ ∅ ∈ Fin) → (∅ LIndF (𝑅 freeLMod ∅) ↔ (∅:dom
∅⟶(Base‘(𝑅 freeLMod ∅)) ∧ ∀𝑥 ∈ dom ∅∀𝑦 ∈
((Base‘(Scalar‘(𝑅 freeLMod ∅))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod ∅)))}) ¬ (𝑦(
·𝑠 ‘(𝑅 freeLMod ∅))(∅‘𝑥)) ∈ ((LSpan‘(𝑅 freeLMod
∅))‘(∅ “ (dom ∅ ∖ {𝑥})))))) |
38 | 30, 15, 37 | mp2an 704 |
. . . . . . . 8
⊢ (∅
LIndF (𝑅 freeLMod ∅)
↔ (∅:dom ∅⟶(Base‘(𝑅 freeLMod ∅)) ∧ ∀𝑥 ∈ dom ∅∀𝑦 ∈
((Base‘(Scalar‘(𝑅 freeLMod ∅))) ∖
{(0g‘(Scalar‘(𝑅 freeLMod ∅)))}) ¬ (𝑦(
·𝑠 ‘(𝑅 freeLMod ∅))(∅‘𝑥)) ∈ ((LSpan‘(𝑅 freeLMod
∅))‘(∅ “ (dom ∅ ∖ {𝑥}))))) |
39 | 27, 29, 38 | mpbir2an 957 |
. . . . . . 7
⊢ ∅
LIndF (𝑅 freeLMod
∅) |
40 | 39 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ Field → ∅
LIndF (𝑅 freeLMod
∅)) |
41 | 23, 40 | 2thd 254 |
. . . . 5
⊢ (𝑅 ∈ Field → (∅
∈ (Unit‘(∅ Mat 𝑅)) ↔ ∅ LIndF (𝑅 freeLMod ∅))) |
42 | 1 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝐼 = ∅ →
(Unit‘(𝐼 Mat 𝑅)) = (Unit‘(∅ Mat
𝑅))) |
43 | | eleq12 2678 |
. . . . . . . 8
⊢ ((𝑀 = ∅ ∧
(Unit‘(𝐼 Mat 𝑅)) = (Unit‘(∅ Mat
𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ∅ ∈
(Unit‘(∅ Mat 𝑅)))) |
44 | 42, 43 | sylan2 490 |
. . . . . . 7
⊢ ((𝑀 = ∅ ∧ 𝐼 = ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ∅ ∈
(Unit‘(∅ Mat 𝑅)))) |
45 | | cureq 32555 |
. . . . . . . . 9
⊢ (𝑀 = ∅ → curry 𝑀 = curry
∅) |
46 | | df-cur 7280 |
. . . . . . . . . 10
⊢ curry
∅ = (𝑥 ∈ dom dom
∅ ↦ {〈𝑦,
𝑧〉 ∣ 〈𝑥, 𝑦〉∅𝑧}) |
47 | 25 | dmeqi 5247 |
. . . . . . . . . . . 12
⊢ dom dom
∅ = dom ∅ |
48 | 47, 25 | eqtri 2632 |
. . . . . . . . . . 11
⊢ dom dom
∅ = ∅ |
49 | | mpteq1 4665 |
. . . . . . . . . . 11
⊢ (dom dom
∅ = ∅ → (𝑥
∈ dom dom ∅ ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉∅𝑧}) = (𝑥 ∈ ∅ ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉∅𝑧})) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom dom ∅ ↦
{〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉∅𝑧}) = (𝑥 ∈ ∅ ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉∅𝑧}) |
51 | | mpt0 5934 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∅ ↦
{〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉∅𝑧}) = ∅ |
52 | 46, 50, 51 | 3eqtri 2636 |
. . . . . . . . 9
⊢ curry
∅ = ∅ |
53 | 45, 52 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑀 = ∅ → curry 𝑀 = ∅) |
54 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝐼 = ∅ → (𝑅 freeLMod 𝐼) = (𝑅 freeLMod ∅)) |
55 | 53, 54 | breqan12d 4599 |
. . . . . . 7
⊢ ((𝑀 = ∅ ∧ 𝐼 = ∅) → (curry 𝑀 LIndF (𝑅 freeLMod 𝐼) ↔ ∅ LIndF (𝑅 freeLMod ∅))) |
56 | 44, 55 | bibi12d 334 |
. . . . . 6
⊢ ((𝑀 = ∅ ∧ 𝐼 = ∅) → ((𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) ↔ (∅ ∈
(Unit‘(∅ Mat 𝑅)) ↔ ∅ LIndF (𝑅 freeLMod ∅)))) |
57 | 56 | biimparc 503 |
. . . . 5
⊢
(((∅ ∈ (Unit‘(∅ Mat 𝑅)) ↔ ∅ LIndF (𝑅 freeLMod ∅)) ∧ (𝑀 = ∅ ∧ 𝐼 = ∅)) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
58 | 41, 57 | sylan 487 |
. . . 4
⊢ ((𝑅 ∈ Field ∧ (𝑀 = ∅ ∧ 𝐼 = ∅)) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
59 | 58 | anassrs 678 |
. . 3
⊢ (((𝑅 ∈ Field ∧ 𝑀 = ∅) ∧ 𝐼 = ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
60 | 9, 59 | sylancom 698 |
. 2
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 = ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
61 | 10 | simprbi 479 |
. . . . 5
⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing) |
62 | | eqid 2610 |
. . . . . 6
⊢ (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅) |
63 | | eqid 2610 |
. . . . . 6
⊢ (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅) |
64 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(𝐼 Mat
𝑅)) = (Base‘(𝐼 Mat 𝑅)) |
65 | | eqid 2610 |
. . . . . 6
⊢
(Unit‘(𝐼 Mat
𝑅)) = (Unit‘(𝐼 Mat 𝑅)) |
66 | | eqid 2610 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
67 | 62, 63, 64, 65, 66 | matunit 20303 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))) |
68 | 61, 67 | sylan 487 |
. . . 4
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))) |
69 | 68 | adantr 480 |
. . 3
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))) |
70 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
71 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
72 | 70, 66, 71 | drngunit 18575 |
. . . . . . . . 9
⊢ (𝑅 ∈ DivRing → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ (((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅)))) |
73 | 11, 72 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Field → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ (((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅)))) |
74 | 73 | adantr 480 |
. . . . . . 7
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ (((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅)))) |
75 | 63, 62, 64, 70 | mdetcl 20221 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅)) |
76 | 61, 75 | sylan 487 |
. . . . . . . 8
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅)) |
77 | 76 | biantrurd 528 |
. . . . . . 7
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) ↔ (((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅) ∧ ((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅)))) |
78 | 74, 77 | bitr4d 270 |
. . . . . 6
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅))) |
79 | 78 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ ((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅))) |
80 | 62, 64 | matrcl 20037 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝐼 ∈ Fin ∧ 𝑅 ∈ V)) |
81 | 80 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → 𝐼 ∈ Fin) |
82 | 81 | pm4.71i 662 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ∈ Fin)) |
83 | | xpfi 8116 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin) |
84 | 83 | anidms 675 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin) |
85 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼)) |
86 | 85, 70 | frlmfibas 19924 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑𝑚
(𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
87 | 84, 86 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) →
((Base‘𝑅)
↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼)))) |
88 | 62, 85 | matbas 20038 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Field) →
(Base‘(𝑅 freeLMod
(𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅))) |
89 | 88 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) →
(Base‘(𝑅 freeLMod
(𝐼 × 𝐼))) = (Base‘(𝐼 Mat 𝑅))) |
90 | 87, 89 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) →
((Base‘𝑅)
↑𝑚 (𝐼 × 𝐼)) = (Base‘(𝐼 Mat 𝑅))) |
91 | 90 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅)))) |
92 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅)
∈ V |
93 | | elmapg 7757 |
. . . . . . . . . . . . . . 15
⊢
(((Base‘𝑅)
∈ V ∧ (𝐼 ×
𝐼) ∈ Fin) →
(𝑀 ∈
((Base‘𝑅)
↑𝑚 (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))) |
94 | 92, 84, 93 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ Fin → (𝑀 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))) |
95 | 94 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))) |
96 | 91, 95 | bitr3d 269 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅))) |
97 | 96 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Field → (𝐼 ∈ Fin → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))) |
98 | 97 | pm5.32rd 670 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Field → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ∈ Fin) ↔ (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin))) |
99 | 82, 98 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝑅 ∈ Field → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin))) |
100 | 99 | biimpd 218 |
. . . . . . . 8
⊢ (𝑅 ∈ Field → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) → (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin))) |
101 | 100 | imdistani 722 |
. . . . . . 7
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑅 ∈ Field ∧ (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin))) |
102 | | anass 679 |
. . . . . . 7
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ Fin) ↔ (𝑅 ∈ Field ∧ (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin))) |
103 | 101, 102 | sylibr 223 |
. . . . . 6
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ Fin)) |
104 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝐼 ∈ (Fin ∖ {∅})
↔ (𝐼 ∈ Fin ∧
𝐼 ≠
∅)) |
105 | | matunitlindflem1 32575 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) →
(¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅))) |
106 | 105 | necon1ad 2799 |
. . . . . . . 8
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) →
(((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
107 | 104, 106 | sylan2br 492 |
. . . . . . 7
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅)) → (((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
108 | 107 | anassrs 678 |
. . . . . 6
⊢ ((((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ Fin) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
109 | 103, 108 | sylan 487 |
. . . . 5
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
110 | 79, 109 | sylbid 229 |
. . . 4
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
111 | | matunitlindflem2 32576 |
. . . . 5
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)) |
112 | 111 | ex 449 |
. . . 4
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))) |
113 | 110, 112 | impbid 201 |
. . 3
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
114 | 69, 113 | bitrd 267 |
. 2
⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |
115 | 60, 114 | pm2.61dane 2869 |
1
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) |