Metamath Proof Explorer

Theorem cramerlem2

Description: Lemma 2 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	cramerlem2	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to \forall z \in V (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		simpll1	$⊢ (((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		simpll2	$⊢ (((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 \in B \land Y \in V)$
9		simpll3	$⊢ (((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 D (X) \in Unit (R)$
10		simplr	$⊢ (((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 \in V$
11		simpr	$⊢ (((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$
12	1 2 3 4 5 6	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))$
13	7 8 9 10 11 12	syl113anc	$⊢ (((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))$
14	13	ex	$⊢ ((R \in CRing \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \land z \in V) \to (X \underset{˙}{\cdot} z = Y \to z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)))$
15	14	ralrimiva	$⊢ (R \in CRing \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to \forall z \in V (X \underset{˙}{\cdot} z = Y \to z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)))$