cvsmuleqdivd

Description: An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)

	Ref	Expression
Hypotheses	cvsdiveqd.v	$⊢ V = {Base}_{W}$
	cvsdiveqd.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	cvsdiveqd.f	$⊢ F = Scalar (W)$
	cvsdiveqd.k	$⊢ K = {Base}_{F}$
	cvsdiveqd.w	$⊢ φ \to W \in ℂVec$
	cvsdiveqd.a	$⊢ φ \to A \in K$
	cvsdiveqd.b	$⊢ φ \to B \in K$
	cvsdiveqd.x	$⊢ φ \to X \in V$
	cvsdiveqd.y	$⊢ φ \to Y \in V$
	cvsdiveqd.1	$⊢ φ \to A \neq 0$
	cvsmuleqdivd.1	$⊢ φ \to A \underset{˙}{\cdot} X = B \underset{˙}{\cdot} Y$
Assertion	cvsmuleqdivd	$⊢ φ \to X = (\frac{B}{A}) \underset{˙}{\cdot} Y$

Proof

Step	Hyp	Ref	Expression
1		cvsdiveqd.v	$⊢ V = {Base}_{W}$
2		cvsdiveqd.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		cvsdiveqd.f	$⊢ F = Scalar (W)$
4		cvsdiveqd.k	$⊢ K = {Base}_{F}$
5		cvsdiveqd.w	$⊢ φ \to W \in ℂVec$
6		cvsdiveqd.a	$⊢ φ \to A \in K$
7		cvsdiveqd.b	$⊢ φ \to B \in K$
8		cvsdiveqd.x	$⊢ φ \to X \in V$
9		cvsdiveqd.y	$⊢ φ \to Y \in V$
10		cvsdiveqd.1	$⊢ φ \to A \neq 0$
11		cvsmuleqdivd.1	$⊢ φ \to A \underset{˙}{\cdot} X = B \underset{˙}{\cdot} Y$
12	11	oveq2d	$⊢ φ \to (\frac{1}{A}) \underset{˙}{\cdot} (A \underset{˙}{\cdot} X) = (\frac{1}{A}) \underset{˙}{\cdot} (B \underset{˙}{\cdot} Y)$
13	5	cvsclm	$⊢ φ \to W \in CMod$
14	3 4	clmsscn	$⊢ W \in CMod \to K \subseteq ℂ$
15	13 14	syl	$⊢ φ \to K \subseteq ℂ$
16	15 6	sseldd	$⊢ φ \to A \in ℂ$
17	16 10	recid2d	$⊢ φ \to (\frac{1}{A}) A = 1$
18	17	oveq1d	$⊢ φ \to (\frac{1}{A}) A \underset{˙}{\cdot} X = 1 \underset{˙}{\cdot} X$
19	3	clm1	$⊢ W \in CMod \to 1 = 1_{F}$
20	13 19	syl	$⊢ φ \to 1 = 1_{F}$
21	3	clmring	$⊢ W \in CMod \to F \in Ring$
22		eqid	$⊢ 1_{F} = 1_{F}$
23	4 22	ringidcl	$⊢ F \in Ring \to 1_{F} \in K$
24	13 21 23	3syl	$⊢ φ \to 1_{F} \in K$
25	20 24	eqeltrd	$⊢ φ \to 1 \in K$
26	3 4	cvsdivcl	$⊢ (W \in ℂVec \land (1 \in K \land A \in K \land A \neq 0)) \to \frac{1}{A} \in K$
27	5 25 6 10 26	syl13anc	$⊢ φ \to \frac{1}{A} \in K$
28	1 3 2 4	clmvsass	$⊢ (W \in CMod \land (\frac{1}{A} \in K \land A \in K \land X \in V)) \to (\frac{1}{A}) A \underset{˙}{\cdot} X = (\frac{1}{A}) \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)$
29	13 27 6 8 28	syl13anc	$⊢ φ \to (\frac{1}{A}) A \underset{˙}{\cdot} X = (\frac{1}{A}) \underset{˙}{\cdot} (A \underset{˙}{\cdot} X)$
30	1 2	clmvs1	$⊢ (W \in CMod \land X \in V) \to 1 \underset{˙}{\cdot} X = X$
31	13 8 30	syl2anc	$⊢ φ \to 1 \underset{˙}{\cdot} X = X$
32	18 29 31	3eqtr3d	$⊢ φ \to (\frac{1}{A}) \underset{˙}{\cdot} (A \underset{˙}{\cdot} X) = X$
33	15 7	sseldd	$⊢ φ \to B \in ℂ$
34	33 16 10	divrec2d	$⊢ φ \to \frac{B}{A} = (\frac{1}{A}) B$
35	34	oveq1d	$⊢ φ \to (\frac{B}{A}) \underset{˙}{\cdot} Y = (\frac{1}{A}) B \underset{˙}{\cdot} Y$
36	1 3 2 4	clmvsass	$⊢ (W \in CMod \land (\frac{1}{A} \in K \land B \in K \land Y \in V)) \to (\frac{1}{A}) B \underset{˙}{\cdot} Y = (\frac{1}{A}) \underset{˙}{\cdot} (B \underset{˙}{\cdot} Y)$
37	13 27 7 9 36	syl13anc	$⊢ φ \to (\frac{1}{A}) B \underset{˙}{\cdot} Y = (\frac{1}{A}) \underset{˙}{\cdot} (B \underset{˙}{\cdot} Y)$
38	35 37	eqtr2d	$⊢ φ \to (\frac{1}{A}) \underset{˙}{\cdot} (B \underset{˙}{\cdot} Y) = (\frac{B}{A}) \underset{˙}{\cdot} Y$
39	12 32 38	3eqtr3d	$⊢ φ \to X = (\frac{B}{A}) \underset{˙}{\cdot} Y$

Metamath Proof Explorer

Theorem cvsmuleqdivd

Proof