cramer0

Description: Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019)

	Ref	Expression
Hypotheses	cramer.a	$⊢ A = N Mat R$
	cramer.b	$⊢ B = {Base}_{A}$
	cramer.v	$⊢ V = {Base}_{R}^{N}$
	cramer.d	$⊢ D = N maDet R$
	cramer.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
	cramer.q	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	cramer0	$⊢ ((N = \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)$

Proof

Step	Hyp	Ref	Expression
1		cramer.a	$⊢ A = N Mat R$
2		cramer.b	$⊢ B = {Base}_{A}$
3		cramer.v	$⊢ V = {Base}_{R}^{N}$
4		cramer.d	$⊢ D = N maDet R$
5		cramer.x	$⊢ \underset{˙}{\cdot} = R maVecMul ⟨N, N⟩$
6		cramer.q	$⊢ \underset{˙}{\times} = /_{r} (R)$
7	1	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
8	2 7	eqtri	$⊢ B = {Base}_{(N Mat R)}$
9		fvoveq1	$⊢ N = \emptyset \to {Base}_{(N Mat R)} = {Base}_{(\emptyset Mat R)}$
10	8 9	syl5eq	$⊢ N = \emptyset \to B = {Base}_{(\emptyset Mat R)}$
11	10	adantr	$⊢ (N = \emptyset \land R \in CRing) \to B = {Base}_{(\emptyset Mat R)}$
12	11	eleq2d	$⊢ (N = \emptyset \land R \in CRing) \to (X \in B \leftrightarrow X \in {Base}_{(\emptyset Mat R)})$
13		mat0dimbas0	$⊢ R \in CRing \to {Base}_{(\emptyset Mat R)} = \{\emptyset\}$
14	13	eleq2d	$⊢ R \in CRing \to (X \in {Base}_{(\emptyset Mat R)} \leftrightarrow X \in \{\emptyset\})$
15	14	adantl	$⊢ (N = \emptyset \land R \in CRing) \to (X \in {Base}_{(\emptyset Mat R)} \leftrightarrow X \in \{\emptyset\})$
16	12 15	bitrd	$⊢ (N = \emptyset \land R \in CRing) \to (X \in B \leftrightarrow X \in \{\emptyset\})$
17	3	a1i	$⊢ (N = \emptyset \land R \in CRing) \to V = {Base}_{R}^{N}$
18		oveq2	$⊢ N = \emptyset \to {Base}_{R}^{N} = {Base}_{R}^{\emptyset}$
19	18	adantr	$⊢ (N = \emptyset \land R \in CRing) \to {Base}_{R}^{N} = {Base}_{R}^{\emptyset}$
20		fvex	$⊢ {Base}_{R} \in V$
21		map0e	$⊢ {Base}_{R} \in V \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
22	20 21	mp1i	$⊢ (N = \emptyset \land R \in CRing) \to {Base}_{R}^{\emptyset} = 1_{𝑜}$
23	17 19 22	3eqtrd	$⊢ (N = \emptyset \land R \in CRing) \to V = 1_{𝑜}$
24	23	eleq2d	$⊢ (N = \emptyset \land R \in CRing) \to (Y \in V \leftrightarrow Y \in 1_{𝑜})$
25		el1o	$⊢ Y \in 1_{𝑜} \leftrightarrow Y = \emptyset$
26	24 25	bitrdi	$⊢ (N = \emptyset \land R \in CRing) \to (Y \in V \leftrightarrow Y = \emptyset)$
27	16 26	anbi12d	$⊢ (N = \emptyset \land R \in CRing) \to ((X \in B \land Y \in V) \leftrightarrow (X \in \{\emptyset\} \land Y = \emptyset))$
28		elsni	$⊢ X \in \{\emptyset\} \to X = \emptyset$
29		mpteq1	$⊢ N = \emptyset \to (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = (i \in \emptyset ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$
30		mpt0	$⊢ (i \in \emptyset ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = \emptyset$
31	29 30	eqtrdi	$⊢ N = \emptyset \to (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = \emptyset$
32	31	eqeq2d	$⊢ N = \emptyset \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \leftrightarrow Z = \emptyset)$
33	32	ad2antrr	$⊢ ((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \leftrightarrow Z = \emptyset)$
34		simplrl	$⊢ (((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \land Z = \emptyset) \to X = \emptyset$
35		simpr	$⊢ (((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \land Z = \emptyset) \to Z = \emptyset$
36	34 35	oveq12d	$⊢ (((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \land Z = \emptyset) \to X \underset{˙}{\cdot} Z = \emptyset \underset{˙}{\cdot} \emptyset$
37	5	mavmul0	$⊢ (N = \emptyset \land R \in CRing) \to \emptyset \underset{˙}{\cdot} \emptyset = \emptyset$
38	37	ad2antrr	$⊢ (((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \land Z = \emptyset) \to \emptyset \underset{˙}{\cdot} \emptyset = \emptyset$
39		simpr	$⊢ (X = \emptyset \land Y = \emptyset) \to Y = \emptyset$
40	39	eqcomd	$⊢ (X = \emptyset \land Y = \emptyset) \to \emptyset = Y$
41	40	ad2antlr	$⊢ (((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \land Z = \emptyset) \to \emptyset = Y$
42	36 38 41	3eqtrd	$⊢ (((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \land Z = \emptyset) \to X \underset{˙}{\cdot} Z = Y$
43	42	ex	$⊢ ((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \to (Z = \emptyset \to X \underset{˙}{\cdot} Z = Y)$
44	33 43	sylbid	$⊢ ((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)$
45	44	a1d	$⊢ ((N = \emptyset \land R \in CRing) \land (X = \emptyset \land Y = \emptyset)) \to (D (X) \in Unit (R) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y))$
46	45	ex	$⊢ (N = \emptyset \land R \in CRing) \to ((X = \emptyset \land Y = \emptyset) \to (D (X) \in Unit (R) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)))$
47	28 46	sylani	$⊢ (N = \emptyset \land R \in CRing) \to ((X \in \{\emptyset\} \land Y = \emptyset) \to (D (X) \in Unit (R) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)))$
48	27 47	sylbid	$⊢ (N = \emptyset \land R \in CRing) \to ((X \in B \land Y \in V) \to (D (X) \in Unit (R) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)))$
49	48	3imp	$⊢ ((N = \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)$

Metamath Proof Explorer

Theorem cramer0

Proof