cramerlem3

Description: Lemma 3 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	cramerlem3	$⊢ ((N \neq \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 2 3 5 4	slesolex	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to \exists v \in V X \underset{˙}{\cdot} v = Y$
8	1 2 3 4 5 6	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)))$
9	8	3adant1l	$⊢ ((N \neq \emptyset \land 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)))$
10		oveq2	$⊢ z = v \to X \underset{˙}{\cdot} z = X \underset{˙}{\cdot} v$
11	10	eqeq1d	$⊢ z = v \to (X \underset{˙}{\cdot} z = Y \leftrightarrow X \underset{˙}{\cdot} v = Y)$
12		oveq2	$⊢ v = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} v = X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$
13	12	eqeq1d	$⊢ v = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to (X \underset{˙}{\cdot} v = Y \leftrightarrow X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y)$
14	11 13	rexraleqim	$⊢ (\exists v \in V X \underset{˙}{\cdot} v = Y \land \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)))) \to X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y$
15		oveq2	$⊢ Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$
16	15	adantl	$⊢ (X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y \land Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))) \to X \underset{˙}{\cdot} Z = X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))$
17		simpl	$⊢ (X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y \land Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))) \to X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y$
18	16 17	eqtrd	$⊢ (X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y \land Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X))) \to X \underset{˙}{\cdot} Z = Y$
19	18	ex	$⊢ X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)$
20	19	a1d	$⊢ X \underset{˙}{\cdot} (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) = Y \to (((N \neq \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))$
21	14 20	syl	$⊢ (\exists v \in V X \underset{˙}{\cdot} v = Y \land \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)))) \to (((N \neq \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))$
22	21	expcom	$⊢ \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))) \to (\exists v \in V X \underset{˙}{\cdot} v = Y \to (((N \neq \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)))$
23	22	com23	$⊢ \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))) \to (((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (\exists v \in V X \underset{˙}{\cdot} v = Y \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y)))$
24	9 23	mpcom	$⊢ ((N \neq \emptyset \land R \in CRing) \land (X \in B \land Y \in V) \land D (X) \in Unit (R)) \to (\exists v \in V X \underset{˙}{\cdot} v = Y \to (Z = (i \in N ⟼ D ((X (N matRepV R) Y) (i)) \underset{˙}{\times} D (X)) \to X \underset{˙}{\cdot} Z = Y))$
25	7 24	mpd	$⊢ ((N \neq \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 cramerlem3

Proof