Theorem matunitlindf 37605

Description: A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.)

Assertion

Ref	Expression
matunitlindf	⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))

Proof of Theorem matunitlindf

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvoveq1 7392	. . . . . . . 8 ⊢ (𝐼 = ∅ → (Base‘(𝐼 Mat 𝑅)) = (Base‘(∅ Mat 𝑅)))
2		mat0dimbas0 22386	. . . . . . . 8 ⊢ (𝑅 ∈ Field → (Base‘(∅ Mat 𝑅)) = {∅})
3	1, 2	sylan9eq 2784	. . . . . . 7 ⊢ ((𝐼 = ∅ ∧ 𝑅 ∈ Field) → (Base‘(𝐼 Mat 𝑅)) = {∅})
4	3	eleq2d 2814	. . . . . 6 ⊢ ((𝐼 = ∅ ∧ 𝑅 ∈ Field) → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ 𝑀 ∈ {∅}))
5		elsni 4602	. . . . . 6 ⊢ (𝑀 ∈ {∅} → 𝑀 = ∅)
6	4, 5	biimtrdi 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 20660	. . . . . . . 8 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
10	9	simplbi 497	. . . . . . 7 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
11		drngring 20656	. . . . . . 7 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
12		eqid 2729	. . . . . . . . 9 ⊢ (∅ Mat 𝑅) = (∅ Mat 𝑅)
13	12	mat0dimid 22388	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (1r‘(∅ Mat 𝑅)) = ∅)
14		0fi 8990	. . . . . . . . . 10 ⊢ ∅ ∈ Fin
15	12	matring 22363	. . . . . . . . . 10 ⊢ ((∅ ∈ Fin ∧ 𝑅 ∈ Ring) → (∅ Mat 𝑅) ∈ Ring)
16	14, 15	mpan 690	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (∅ Mat 𝑅) ∈ Ring)
17		eqid 2729	. . . . . . . . . 10 ⊢ (Unit‘(∅ Mat 𝑅)) = (Unit‘(∅ Mat 𝑅))
18		eqid 2729	. . . . . . . . . 10 ⊢ (1r‘(∅ Mat 𝑅)) = (1r‘(∅ Mat 𝑅))
19	17, 18	1unit 20294	. . . . . . . . 9 ⊢ ((∅ Mat 𝑅) ∈ Ring → (1r‘(∅ Mat 𝑅)) ∈ (Unit‘(∅ Mat 𝑅)))
20	16, 19	syl 17	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (1r‘(∅ Mat 𝑅)) ∈ (Unit‘(∅ Mat 𝑅)))
21	13, 20	eqeltrrd 2829	. . . . . . 7 ⊢ (𝑅 ∈ Ring → ∅ ∈ (Unit‘(∅ Mat 𝑅)))
22	10, 11, 21	3syl 18	. . . . . 6 ⊢ (𝑅 ∈ Field → ∅ ∈ (Unit‘(∅ Mat 𝑅)))
23		f0 6723	. . . . . . . . 9 ⊢ ∅:∅⟶(Base‘(𝑅 freeLMod ∅))
24		dm0 5874	. . . . . . . . . 10 ⊢ dom ∅ = ∅
25	24	feq2i 6662	. . . . . . . . 9 ⊢ (∅:dom ∅⟶(Base‘(𝑅 freeLMod ∅)) ↔ ∅:∅⟶(Base‘(𝑅 freeLMod ∅)))
26	23, 25	mpbir 231	. . . . . . . 8 ⊢ ∅:dom ∅⟶(Base‘(𝑅 freeLMod ∅))
27		rzal 4468	. . . . . . . . 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 7402	. . . . . . . . 9 ⊢ (𝑅 freeLMod ∅) ∈ V
30		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘(𝑅 freeLMod ∅)) = (Base‘(𝑅 freeLMod ∅))
31		eqid 2729	. . . . . . . . . 10 ⊢ ( ·𝑠 ‘(𝑅 freeLMod ∅)) = ( ·𝑠 ‘(𝑅 freeLMod ∅))
32		eqid 2729	. . . . . . . . . 10 ⊢ (LSpan‘(𝑅 freeLMod ∅)) = (LSpan‘(𝑅 freeLMod ∅))
33		eqid 2729	. . . . . . . . . 10 ⊢ (Scalar‘(𝑅 freeLMod ∅)) = (Scalar‘(𝑅 freeLMod ∅))
34		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘(Scalar‘(𝑅 freeLMod ∅))) = (Base‘(Scalar‘(𝑅 freeLMod ∅)))
35		eqid 2729	. . . . . . . . . 10 ⊢ (0g‘(Scalar‘(𝑅 freeLMod ∅))) = (0g‘(Scalar‘(𝑅 freeLMod ∅)))
36	30, 31, 32, 33, 34, 35	islindf 21754	. . . . . . . . 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 692	. . . . . . . 8 ⊢ (∅ LIndF (𝑅 freeLMod ∅) ↔ (∅:dom ∅⟶(Base‘(𝑅 freeLMod ∅)) ∧ ∀𝑥 ∈ dom ∅∀𝑦 ∈ ((Base‘(Scalar‘(𝑅 freeLMod ∅))) ∖ {(0g‘(Scalar‘(𝑅 freeLMod ∅)))}) ¬ (𝑦( ·𝑠 ‘(𝑅 freeLMod ∅))(∅‘𝑥)) ∈ ((LSpan‘(𝑅 freeLMod ∅))‘(∅ “ (dom ∅ ∖ {𝑥})))))
38	26, 28, 37	mpbir2an 711	. . . . . . 7 ⊢ ∅ LIndF (𝑅 freeLMod ∅)
39	38	a1i 11	. . . . . 6 ⊢ (𝑅 ∈ Field → ∅ LIndF (𝑅 freeLMod ∅))
40	22, 39	2thd 265	. . . . 5 ⊢ (𝑅 ∈ Field → (∅ ∈ (Unit‘(∅ Mat 𝑅)) ↔ ∅ LIndF (𝑅 freeLMod ∅)))
41		fvoveq1 7392	. . . . . . . 8 ⊢ (𝐼 = ∅ → (Unit‘(𝐼 Mat 𝑅)) = (Unit‘(∅ Mat 𝑅)))
42		eleq12 2818	. . . . . . . 8 ⊢ ((𝑀 = ∅ ∧ (Unit‘(𝐼 Mat 𝑅)) = (Unit‘(∅ Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ∅ ∈ (Unit‘(∅ Mat 𝑅))))
43	41, 42	sylan2 593	. . . . . . 7 ⊢ ((𝑀 = ∅ ∧ 𝐼 = ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ∅ ∈ (Unit‘(∅ Mat 𝑅))))
44		cureq 37583	. . . . . . . . 9 ⊢ (𝑀 = ∅ → curry 𝑀 = curry ∅)
45		df-cur 8223	. . . . . . . . . 10 ⊢ curry ∅ = (𝑥 ∈ dom dom ∅ ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩∅𝑧})
46	24	dmeqi 5858	. . . . . . . . . . . 12 ⊢ dom dom ∅ = dom ∅
47	46, 24	eqtri 2752	. . . . . . . . . . 11 ⊢ dom dom ∅ = ∅
48		mpteq1 5191	. . . . . . . . . . 11 ⊢ (dom dom ∅ = ∅ → (𝑥 ∈ dom dom ∅ ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩∅𝑧}) = (𝑥 ∈ ∅ ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩∅𝑧}))
49	47, 48	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom dom ∅ ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩∅𝑧}) = (𝑥 ∈ ∅ ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩∅𝑧})
50		mpt0 6642	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∅ ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩∅𝑧}) = ∅
51	45, 49, 50	3eqtri 2756	. . . . . . . . 9 ⊢ curry ∅ = ∅
52	44, 51	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑀 = ∅ → curry 𝑀 = ∅)
53		oveq2 7377	. . . . . . . 8 ⊢ (𝐼 = ∅ → (𝑅 freeLMod 𝐼) = (𝑅 freeLMod ∅))
54	52, 53	breqan12d 5118	. . . . . . 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 580	. . . 4 ⊢ ((𝑅 ∈ Field ∧ (𝑀 = ∅ ∧ 𝐼 = ∅)) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
58	57	anassrs 467	. . 3 ⊢ (((𝑅 ∈ Field ∧ 𝑀 = ∅) ∧ 𝐼 = ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
59	8, 58	sylancom 588	. 2 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 = ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
60	9	simprbi 496	. . . . 5 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
61		eqid 2729	. . . . . 6 ⊢ (𝐼 Mat 𝑅) = (𝐼 Mat 𝑅)
62		eqid 2729	. . . . . 6 ⊢ (𝐼 maDet 𝑅) = (𝐼 maDet 𝑅)
63		eqid 2729	. . . . . 6 ⊢ (Base‘(𝐼 Mat 𝑅)) = (Base‘(𝐼 Mat 𝑅))
64		eqid 2729	. . . . . 6 ⊢ (Unit‘(𝐼 Mat 𝑅)) = (Unit‘(𝐼 Mat 𝑅))
65		eqid 2729	. . . . . 6 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
66	61, 62, 63, 64, 65	matunit 22598	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
67	60, 66	sylan 580	. . . 4 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
68	67	adantr 480	. . 3 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)))
69		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
70		eqid 2729	. . . . . . . . . 10 ⊢ (0g‘𝑅) = (0g‘𝑅)
71	69, 65, 70	drngunit 20654	. . . . . . . . 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 22516	. . . . . . . . 9 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Base‘𝑅))
75	60, 74	sylan 580	. . . . . . . 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 22332	. . . . . . . . . . . 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 9245	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ Fin ∧ 𝐼 ∈ Fin) → (𝐼 × 𝐼) ∈ Fin)
83	82	anidms 566	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ Fin → (𝐼 × 𝐼) ∈ Fin)
84		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 freeLMod (𝐼 × 𝐼)) = (𝑅 freeLMod (𝐼 × 𝐼))
85	84, 69	frlmfibas 21704	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Field ∧ (𝐼 × 𝐼) ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
86	83, 85	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → ((Base‘𝑅) ↑m (𝐼 × 𝐼)) = (Base‘(𝑅 freeLMod (𝐼 × 𝐼))))
87	61, 84	matbas 22333	. . . . . . . . . . . . . . . 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 2814	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Field ∧ 𝐼 ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))))
91		fvex 6853	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑅) ∈ V
92		elmapg 8789	. . . . . . . . . . . . . . 15 ⊢ (((Base‘𝑅) ∈ V ∧ (𝐼 × 𝐼) ∈ Fin) → (𝑀 ∈ ((Base‘𝑅) ↑m (𝐼 × 𝐼)) ↔ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)))
93	91, 83, 92	sylancr 587	. . . . . . . . . . . . . 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 578	. . . . . . . . . 10 ⊢ (𝑅 ∈ Field → ((𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ∧ 𝐼 ∈ Fin) ↔ (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin)))
98	81, 97	bitrid 283	. . . . . . . . 9 ⊢ (𝑅 ∈ Field → (𝑀 ∈ (Base‘(𝐼 Mat 𝑅)) ↔ (𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅) ∧ 𝐼 ∈ Fin)))
99	98	biimpd 229	. . . . . . . 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 234	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → ((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ Fin))
103		eldifsn 4746	. . . . . . . 8 ⊢ (𝐼 ∈ (Fin ∖ {∅}) ↔ (𝐼 ∈ Fin ∧ 𝐼 ≠ ∅))
104		matunitlindflem1 37603	. . . . . . . . 9 ⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅)))
105	104	necon1ad 2942	. . . . . . . 8 ⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
106	103, 105	sylan2br 595	. . . . . . 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 580	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ≠ (0g‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
109	78, 108	sylbid 240	. . . 4 ⊢ (((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) → (((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅) → curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
110		matunitlindflem2 37604	. . . . 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 212	. . 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 3012	1 ⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  Vcvv 3444   ∖ cdif 3908  ∅c0 4292  {csn 4585  ⟨cop 4591   class class class wbr 5102  {copab 5164   ↦ cmpt 5183   × cxp 5629  dom cdm 5631   “ cima 5634  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369  curry ccur 8221   ↑_m cmap 8776  Fincfn 8895  Basecbs 17155  Scalarcsca 17199   ·_𝑠 cvsca 17200  0_gc0g 17378  1_rcur 20101  Ringcrg 20153  CRingccrg 20154  Unitcui 20275  DivRingcdr 20649  Fieldcfield 20650  LSpanclspn 20909   freeLMod cfrlm 21688   LIndF clindf 21746   Mat cmat 22327   maDet cmdat 22504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-addf 11123  ax-mulf 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-ot 4594  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-tpos 8182  df-cur 8223  df-unc 8224  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-sup 9369  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-xnn0 12492  df-z 12506  df-dec 12626  df-uz 12770  df-rp 12928  df-fz 13445  df-fzo 13592  df-seq 13943  df-exp 14003  df-hash 14272  df-word 14455  df-lsw 14504  df-concat 14512  df-s1 14537  df-substr 14582  df-pfx 14612  df-splice 14691  df-reverse 14700  df-s2 14790  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-0g 17380  df-gsum 17381  df-prds 17386  df-pws 17388  df-mre 17523  df-mrc 17524  df-mri 17525  df-acs 17526  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-mhm 18692  df-submnd 18693  df-efmnd 18778  df-grp 18850  df-minusg 18851  df-sbg 18852  df-mulg 18982  df-subg 19037  df-ghm 19127  df-gim 19173  df-cntz 19231  df-oppg 19260  df-symg 19284  df-pmtr 19356  df-psgn 19405  df-evpm 19406  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-srg 20107  df-ring 20155  df-cring 20156  df-oppr 20257  df-dvdsr 20277  df-unit 20278  df-invr 20308  df-dvr 20321  df-rhm 20392  df-nzr 20433  df-subrng 20466  df-subrg 20490  df-drng 20651  df-field 20652  df-lmod 20800  df-lss 20870  df-lsp 20910  df-lmhm 20961  df-lbs 21014  df-lvec 21042  df-sra 21112  df-rgmod 21113  df-cnfld 21297  df-zring 21389  df-zrh 21445  df-dsmm 21674  df-frlm 21689  df-uvc 21725  df-lindf 21748  df-linds 21749  df-assa 21795  df-mamu 22311  df-mat 22328  df-mdet 22505  df-madu 22554

This theorem is referenced by: (None)