matunitlindf

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

		Ref	Expression
	Assertion	matunitlindf	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	$⊢ I = \emptyset \to {Base}_{(I Mat R)} = {Base}_{(\emptyset Mat R)}$
2		mat0dimbas0	$⊢ R \in Field \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
3	1 2	sylan9eq	$⊢ (I = \emptyset \land R \in Field) \to {Base}_{(I Mat R)} = \{\emptyset\}$
4	3	eleq2d	$⊢ (I = \emptyset \land R \in Field) \to (M \in {Base}_{(I Mat R)} \leftrightarrow M \in \{\emptyset\})$
5		elsni	$⊢ M \in \{\emptyset\} \to M = \emptyset$
6	4 5	syl6bi	$⊢ (I = \emptyset \land R \in Field) \to (M \in {Base}_{(I Mat R)} \to M = \emptyset)$
7	6	imdistanda	$⊢ I = \emptyset \to ((R \in Field \land M \in {Base}_{(I Mat R)}) \to (R \in Field \land M = \emptyset))$
8	7	impcom	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I = \emptyset) \to (R \in Field \land M = \emptyset)$
9		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
10	9	simplbi	$⊢ R \in Field \to R \in DivRing$
11		drngring	$⊢ R \in DivRing \to R \in Ring$
12		eqid	$⊢ \emptyset Mat R = \emptyset Mat R$
13	12	mat0dimid	$⊢ R \in Ring \to 1_{(\emptyset Mat R)} = \emptyset$
14		0fin	$⊢ \emptyset \in Fin$
15	12	matring	$⊢ (\emptyset \in Fin \land R \in Ring) \to \emptyset Mat R \in Ring$
16	14 15	mpan	$⊢ R \in Ring \to \emptyset Mat R \in Ring$
17		eqid	$⊢ Unit (\emptyset Mat R) = Unit (\emptyset Mat R)$
18		eqid	$⊢ 1_{(\emptyset Mat R)} = 1_{(\emptyset Mat R)}$
19	17 18	1unit	$⊢ \emptyset Mat R \in Ring \to 1_{(\emptyset Mat R)} \in Unit (\emptyset Mat R)$
20	16 19	syl	$⊢ R \in Ring \to 1_{(\emptyset Mat R)} \in Unit (\emptyset Mat R)$
21	13 20	eqeltrrd	$⊢ R \in Ring \to \emptyset \in Unit (\emptyset Mat R)$
22	10 11 21	3syl	$⊢ R \in Field \to \emptyset \in Unit (\emptyset Mat R)$
23		f0	$⊢ \emptyset : \emptyset ⟶ {Base}_{(R freeLMod \emptyset)}$
24		dm0	$⊢ dom \emptyset = \emptyset$
25	24	feq2i	$⊢ \emptyset : dom \emptyset ⟶ {Base}_{(R freeLMod \emptyset)} \leftrightarrow \emptyset : \emptyset ⟶ {Base}_{(R freeLMod \emptyset)}$
26	23 25	mpbir	$⊢ \emptyset : dom \emptyset ⟶ {Base}_{(R freeLMod \emptyset)}$
27		rzal	$⊢ dom \emptyset = \emptyset \to \forall x \in dom \emptyset \forall y \in ({Base}_{Scalar (R freeLMod \emptyset)} ∖ \{0_{Scalar (R freeLMod \emptyset)}\}) \neg y \cdot_{(R freeLMod \emptyset)} \emptyset (x) \in LSpan (R freeLMod \emptyset) (\emptyset [dom \emptyset ∖ \{x\}])$
28	24 27	ax-mp	$⊢ \forall x \in dom \emptyset \forall y \in ({Base}_{Scalar (R freeLMod \emptyset)} ∖ \{0_{Scalar (R freeLMod \emptyset)}\}) \neg y \cdot_{(R freeLMod \emptyset)} \emptyset (x) \in LSpan (R freeLMod \emptyset) (\emptyset [dom \emptyset ∖ \{x\}])$
29		ovex	$⊢ R freeLMod \emptyset \in V$
30		eqid	$⊢ {Base}_{(R freeLMod \emptyset)} = {Base}_{(R freeLMod \emptyset)}$
31		eqid	$⊢ \cdot_{(R freeLMod \emptyset)} = \cdot_{(R freeLMod \emptyset)}$
32		eqid	$⊢ LSpan (R freeLMod \emptyset) = LSpan (R freeLMod \emptyset)$
33		eqid	$⊢ Scalar (R freeLMod \emptyset) = Scalar (R freeLMod \emptyset)$
34		eqid	$⊢ {Base}_{Scalar (R freeLMod \emptyset)} = {Base}_{Scalar (R freeLMod \emptyset)}$
35		eqid	$⊢ 0_{Scalar (R freeLMod \emptyset)} = 0_{Scalar (R freeLMod \emptyset)}$
36	30 31 32 33 34 35	islindf	$⊢ (R freeLMod \emptyset \in V \land \emptyset \in Fin) \to (\emptyset LIndF (R freeLMod \emptyset) \leftrightarrow (\emptyset : dom \emptyset ⟶ {Base}_{(R freeLMod \emptyset)} \land \forall x \in dom \emptyset \forall y \in ({Base}_{Scalar (R freeLMod \emptyset)} ∖ \{0_{Scalar (R freeLMod \emptyset)}\}) \neg y \cdot_{(R freeLMod \emptyset)} \emptyset (x) \in LSpan (R freeLMod \emptyset) (\emptyset [dom \emptyset ∖ \{x\}])))$
37	29 14 36	mp2an	$⊢ \emptyset LIndF (R freeLMod \emptyset) \leftrightarrow (\emptyset : dom \emptyset ⟶ {Base}_{(R freeLMod \emptyset)} \land \forall x \in dom \emptyset \forall y \in ({Base}_{Scalar (R freeLMod \emptyset)} ∖ \{0_{Scalar (R freeLMod \emptyset)}\}) \neg y \cdot_{(R freeLMod \emptyset)} \emptyset (x) \in LSpan (R freeLMod \emptyset) (\emptyset [dom \emptyset ∖ \{x\}]))$
38	26 28 37	mpbir2an	$⊢ \emptyset LIndF (R freeLMod \emptyset)$
39	38	a1i	$⊢ R \in Field \to \emptyset LIndF (R freeLMod \emptyset)$
40	22 39	2thd	$⊢ R \in Field \to (\emptyset \in Unit (\emptyset Mat R) \leftrightarrow \emptyset LIndF (R freeLMod \emptyset))$
41		fvoveq1	$⊢ I = \emptyset \to Unit (I Mat R) = Unit (\emptyset Mat R)$
42		eleq12	$⊢ (M = \emptyset \land Unit (I Mat R) = Unit (\emptyset Mat R)) \to (M \in Unit (I Mat R) \leftrightarrow \emptyset \in Unit (\emptyset Mat R))$
43	41 42	sylan2	$⊢ (M = \emptyset \land I = \emptyset) \to (M \in Unit (I Mat R) \leftrightarrow \emptyset \in Unit (\emptyset Mat R))$
44		cureq	$⊢ M = \emptyset \to curry M = curry \emptyset$
45		df-cur	$⊢ curry \emptyset = (x \in dom dom \emptyset ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ \emptyset z\})$
46	24	dmeqi	$⊢ dom dom \emptyset = dom \emptyset$
47	46 24	eqtri	$⊢ dom dom \emptyset = \emptyset$
48		mpteq1	$⊢ dom dom \emptyset = \emptyset \to (x \in dom dom \emptyset ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ \emptyset z\}) = (x \in \emptyset ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ \emptyset z\})$
49	47 48	ax-mp	$⊢ (x \in dom dom \emptyset ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ \emptyset z\}) = (x \in \emptyset ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ \emptyset z\})$
50		mpt0	$⊢ (x \in \emptyset ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ \emptyset z\}) = \emptyset$
51	45 49 50	3eqtri	$⊢ curry \emptyset = \emptyset$
52	44 51	syl6eq	$⊢ M = \emptyset \to curry M = \emptyset$
53		oveq2	$⊢ I = \emptyset \to R freeLMod I = R freeLMod \emptyset$
54	52 53	breqan12d	$⊢ (M = \emptyset \land I = \emptyset) \to (curry M LIndF (R freeLMod I) \leftrightarrow \emptyset LIndF (R freeLMod \emptyset))$
55	43 54	bibi12d	$⊢ (M = \emptyset \land I = \emptyset) \to ((M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I)) \leftrightarrow (\emptyset \in Unit (\emptyset Mat R) \leftrightarrow \emptyset LIndF (R freeLMod \emptyset)))$
56	55	biimparc	$⊢ ((\emptyset \in Unit (\emptyset Mat R) \leftrightarrow \emptyset LIndF (R freeLMod \emptyset)) \land (M = \emptyset \land I = \emptyset)) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$
57	40 56	sylan	$⊢ (R \in Field \land (M = \emptyset \land I = \emptyset)) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$
58	57	anassrs	$⊢ ((R \in Field \land M = \emptyset) \land I = \emptyset) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$
59	8 58	sylancom	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I = \emptyset) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$
60	9	simprbi	$⊢ R \in Field \to R \in CRing$
61		eqid	$⊢ I Mat R = I Mat R$
62		eqid	$⊢ I maDet R = I maDet R$
63		eqid	$⊢ {Base}_{(I Mat R)} = {Base}_{(I Mat R)}$
64		eqid	$⊢ Unit (I Mat R) = Unit (I Mat R)$
65		eqid	$⊢ Unit (R) = Unit (R)$
66	61 62 63 64 65	matunit	$⊢ (R \in CRing \land M \in {Base}_{(I Mat R)}) \to (M \in Unit (I Mat R) \leftrightarrow (I maDet R) (M) \in Unit (R))$
67	60 66	sylan	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to (M \in Unit (I Mat R) \leftrightarrow (I maDet R) (M) \in Unit (R))$
68	67	adantr	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to (M \in Unit (I Mat R) \leftrightarrow (I maDet R) (M) \in Unit (R))$
69		eqid	$⊢ {Base}_{R} = {Base}_{R}$
70		eqid	$⊢ 0_{R} = 0_{R}$
71	69 65 70	drngunit	$⊢ R \in DivRing \to ((I maDet R) (M) \in Unit (R) \leftrightarrow ((I maDet R) (M) \in {Base}_{R} \land (I maDet R) (M) \neq 0_{R}))$
72	10 71	syl	$⊢ R \in Field \to ((I maDet R) (M) \in Unit (R) \leftrightarrow ((I maDet R) (M) \in {Base}_{R} \land (I maDet R) (M) \neq 0_{R}))$
73	72	adantr	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to ((I maDet R) (M) \in Unit (R) \leftrightarrow ((I maDet R) (M) \in {Base}_{R} \land (I maDet R) (M) \neq 0_{R}))$
74	62 61 63 69	mdetcl	$⊢ (R \in CRing \land M \in {Base}_{(I Mat R)}) \to (I maDet R) (M) \in {Base}_{R}$
75	60 74	sylan	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to (I maDet R) (M) \in {Base}_{R}$
76	75	biantrurd	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to ((I maDet R) (M) \neq 0_{R} \leftrightarrow ((I maDet R) (M) \in {Base}_{R} \land (I maDet R) (M) \neq 0_{R}))$
77	73 76	bitr4d	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to ((I maDet R) (M) \in Unit (R) \leftrightarrow (I maDet R) (M) \neq 0_{R})$
78	77	adantr	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to ((I maDet R) (M) \in Unit (R) \leftrightarrow (I maDet R) (M) \neq 0_{R})$
79	61 63	matrcl	$⊢ M \in {Base}_{(I Mat R)} \to (I \in Fin \land R \in V)$
80	79	simpld	$⊢ M \in {Base}_{(I Mat R)} \to I \in Fin$
81	80	pm4.71i	$⊢ M \in {Base}_{(I Mat R)} \leftrightarrow (M \in {Base}_{(I Mat R)} \land I \in Fin)$
82		xpfi	$⊢ (I \in Fin \land I \in Fin) \to I \times I \in Fin$
83	82	anidms	$⊢ I \in Fin \to I \times I \in Fin$
84		eqid	$⊢ R freeLMod (I \times I) = R freeLMod (I \times I)$
85	84 69	frlmfibas	$⊢ (R \in Field \land I \times I \in Fin) \to {Base}_{R}^{(I \times I)} = {Base}_{(R freeLMod (I \times I))}$
86	83 85	sylan2	$⊢ (R \in Field \land I \in Fin) \to {Base}_{R}^{(I \times I)} = {Base}_{(R freeLMod (I \times I))}$
87	61 84	matbas	$⊢ (I \in Fin \land R \in Field) \to {Base}_{(R freeLMod (I \times I))} = {Base}_{(I Mat R)}$
88	87	ancoms	$⊢ (R \in Field \land I \in Fin) \to {Base}_{(R freeLMod (I \times I))} = {Base}_{(I Mat R)}$
89	86 88	eqtrd	$⊢ (R \in Field \land I \in Fin) \to {Base}_{R}^{(I \times I)} = {Base}_{(I Mat R)}$
90	89	eleq2d	$⊢ (R \in Field \land I \in Fin) \to (M \in ({Base}_{R}^{(I \times I)}) \leftrightarrow M \in {Base}_{(I Mat R)})$
91		fvex	$⊢ {Base}_{R} \in V$
92		elmapg	$⊢ ({Base}_{R} \in V \land I \times I \in Fin) \to (M \in ({Base}_{R}^{(I \times I)}) \leftrightarrow M : I \times I ⟶ {Base}_{R})$
93	91 83 92	sylancr	$⊢ I \in Fin \to (M \in ({Base}_{R}^{(I \times I)}) \leftrightarrow M : I \times I ⟶ {Base}_{R})$
94	93	adantl	$⊢ (R \in Field \land I \in Fin) \to (M \in ({Base}_{R}^{(I \times I)}) \leftrightarrow M : I \times I ⟶ {Base}_{R})$
95	90 94	bitr3d	$⊢ (R \in Field \land I \in Fin) \to (M \in {Base}_{(I Mat R)} \leftrightarrow M : I \times I ⟶ {Base}_{R})$
96	95	ex	$⊢ R \in Field \to (I \in Fin \to (M \in {Base}_{(I Mat R)} \leftrightarrow M : I \times I ⟶ {Base}_{R}))$
97	96	pm5.32rd	$⊢ R \in Field \to ((M \in {Base}_{(I Mat R)} \land I \in Fin) \leftrightarrow (M : I \times I ⟶ {Base}_{R} \land I \in Fin))$
98	81 97	syl5bb	$⊢ R \in Field \to (M \in {Base}_{(I Mat R)} \leftrightarrow (M : I \times I ⟶ {Base}_{R} \land I \in Fin))$
99	98	biimpd	$⊢ R \in Field \to (M \in {Base}_{(I Mat R)} \to (M : I \times I ⟶ {Base}_{R} \land I \in Fin))$
100	99	imdistani	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to (R \in Field \land (M : I \times I ⟶ {Base}_{R} \land I \in Fin))$
101		anass	$⊢ ((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land I \in Fin) \leftrightarrow (R \in Field \land (M : I \times I ⟶ {Base}_{R} \land I \in Fin))$
102	100 101	sylibr	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to ((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land I \in Fin)$
103		eldifsn	$⊢ I \in (Fin ∖ \{\emptyset\}) \leftrightarrow (I \in Fin \land I \neq \emptyset)$
104		matunitlindflem1	$⊢ ((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land I \in (Fin ∖ \{\emptyset\})) \to (\neg curry M LIndF (R freeLMod I) \to (I maDet R) (M) = 0_{R})$
105	104	necon1ad	$⊢ ((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land I \in (Fin ∖ \{\emptyset\})) \to ((I maDet R) (M) \neq 0_{R} \to curry M LIndF (R freeLMod I))$
106	103 105	sylan2br	$⊢ ((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land (I \in Fin \land I \neq \emptyset)) \to ((I maDet R) (M) \neq 0_{R} \to curry M LIndF (R freeLMod I))$
107	106	anassrs	$⊢ (((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land I \in Fin) \land I \neq \emptyset) \to ((I maDet R) (M) \neq 0_{R} \to curry M LIndF (R freeLMod I))$
108	102 107	sylan	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to ((I maDet R) (M) \neq 0_{R} \to curry M LIndF (R freeLMod I))$
109	78 108	sylbid	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to ((I maDet R) (M) \in Unit (R) \to curry M LIndF (R freeLMod I))$
110		matunitlindflem2	$⊢ (((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \land curry M LIndF (R freeLMod I)) \to (I maDet R) (M) \in Unit (R)$
111	110	ex	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to (curry M LIndF (R freeLMod I) \to (I maDet R) (M) \in Unit (R))$
112	109 111	impbid	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to ((I maDet R) (M) \in Unit (R) \leftrightarrow curry M LIndF (R freeLMod I))$
113	68 112	bitrd	$⊢ ((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$
114	59 113	pm2.61dane	$⊢ (R \in Field \land M \in {Base}_{(I Mat R)}) \to (M \in Unit (I Mat R) \leftrightarrow curry M LIndF (R freeLMod I))$

Metamath Proof Explorer

Theorem matunitlindf

Proof