cramerlem1

Description: Lemma 1 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 1-Mar-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	cramerlem1	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$

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		simp1	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to R \in CRing$
8	7	anim1i	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \land a \in N) \to (R \in CRing \land a \in N)$
9		simpl2	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \land a \in N) \to (X \in B \land Y \in V)$
10		pm3.22	$⊢ (D (X) \in Unit (R) \land X \underset{˙}{\cdot} Z = Y) \to (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))$
11	10	3adant2	$⊢ (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y) \to (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))$
12	11	3ad2ant3	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))$
13	12	adantr	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \land a \in N) \to (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))$
14		eqid	$⊢ (1_{A} (N matRepV R) Z) (a) = (1_{A} (N matRepV R) Z) (a)$
15		eqid	$⊢ (X (N matRepV R) Y) (a) = (X (N matRepV R) Y) (a)$
16	1 2 3 14 15 5 4 6	cramerimp	$⊢ ((R \in CRing \land a \in N) \land (X \in B \land Y \in V) \land (X \underset{˙}{\cdot} Z = Y \land D (X) \in Unit (R))) \to Z (a) = D ((X (N matRepV R) Y) (a)) \underset{˙}{\times} D (X)$
17	8 9 13 16	syl3anc	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \land a \in N) \to Z (a) = D ((X (N matRepV R) Y) (a)) \underset{˙}{\times} D (X)$
18	17	ralrimiva	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to \forall a \in N Z (a) = D ((X (N matRepV R) Y) (a)) \underset{˙}{\times} D (X)$
19		elmapfn	$⊢ Z \in ({Base}_{R}^{N}) \to Z Fn N$
20	19 3	eleq2s	$⊢ Z \in V \to Z Fn N$
21	20	3ad2ant2	$⊢ (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y) \to Z Fn N$
22	21	3ad2ant3	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to Z Fn N$
23		2fveq3	$⊢ a = i \to D ((X (N matRepV R) Y) (a)) = D ((X (N matRepV R) Y) (i))$
24	23	oveq1d	$⊢ a = i \to D ((X (N matRepV R) Y) (a)) \underset{˙}{\times} D (X) = D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)$
25		ovexd	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \land a \in N) \to D ((X (N matRepV R) Y) (a)) \underset{˙}{\times} D (X) \in V$
26		ovexd	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \land i \in N) \to D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X) \in V$
27	22 24 25 26	fnmptfvd	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \leftrightarrow \forall a \in N Z (a) = D ((X (N matRepV R) Y) (a)) \underset{˙}{\times} D (X))$
28	18 27	mpbird	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land (D (X) \in Unit (R) \land Z \in V \land X \underset{˙}{\cdot} Z = Y)) \to Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$

Metamath Proof Explorer

Theorem cramerlem1

Proof