cvsdiveqd

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$
	cvsdiveqd.2	$⊢ φ \to B \neq 0$
	cvsdiveqd.3	$⊢ φ \to X = (\frac{A}{B}) \underset{˙}{\cdot} Y$
Assertion	cvsdiveqd	$⊢ φ \to (\frac{B}{A}) \underset{˙}{\cdot} X = 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		cvsdiveqd.2	$⊢ φ \to B \neq 0$
12		cvsdiveqd.3	$⊢ φ \to X = (\frac{A}{B}) \underset{˙}{\cdot} Y$
13	12	oveq2d	$⊢ φ \to (\frac{B}{A}) \underset{˙}{\cdot} X = (\frac{B}{A}) \underset{˙}{\cdot} ((\frac{A}{B}) \underset{˙}{\cdot} Y)$
14	5	cvsclm	$⊢ φ \to W \in CMod$
15	3 4	clmsscn	$⊢ W \in CMod \to K \subseteq ℂ$
16	14 15	syl	$⊢ φ \to K \subseteq ℂ$
17	16 7	sseldd	$⊢ φ \to B \in ℂ$
18	16 6	sseldd	$⊢ φ \to A \in ℂ$
19	17 18 11 10	divcan6d	$⊢ φ \to (\frac{B}{A}) (\frac{A}{B}) = 1$
20	19	oveq1d	$⊢ φ \to (\frac{B}{A}) (\frac{A}{B}) \underset{˙}{\cdot} Y = 1 \underset{˙}{\cdot} Y$
21	3 4	cvsdivcl	$⊢ (W \in ℂVec \land (B \in K \land A \in K \land A \neq 0)) \to \frac{B}{A} \in K$
22	5 7 6 10 21	syl13anc	$⊢ φ \to \frac{B}{A} \in K$
23	3 4	cvsdivcl	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} \in K$
24	5 6 7 11 23	syl13anc	$⊢ φ \to \frac{A}{B} \in K$
25	1 3 2 4	clmvsass	$⊢ (W \in CMod \land (\frac{B}{A} \in K \land \frac{A}{B} \in K \land Y \in V)) \to (\frac{B}{A}) (\frac{A}{B}) \underset{˙}{\cdot} Y = (\frac{B}{A}) \underset{˙}{\cdot} ((\frac{A}{B}) \underset{˙}{\cdot} Y)$
26	14 22 24 9 25	syl13anc	$⊢ φ \to (\frac{B}{A}) (\frac{A}{B}) \underset{˙}{\cdot} Y = (\frac{B}{A}) \underset{˙}{\cdot} ((\frac{A}{B}) \underset{˙}{\cdot} Y)$
27	1 2	clmvs1	$⊢ (W \in CMod \land Y \in V) \to 1 \underset{˙}{\cdot} Y = Y$
28	14 9 27	syl2anc	$⊢ φ \to 1 \underset{˙}{\cdot} Y = Y$
29	20 26 28	3eqtr3d	$⊢ φ \to (\frac{B}{A}) \underset{˙}{\cdot} ((\frac{A}{B}) \underset{˙}{\cdot} Y) = Y$
30	13 29	eqtrd	$⊢ φ \to (\frac{B}{A}) \underset{˙}{\cdot} X = Y$

Metamath Proof Explorer

Theorem cvsdiveqd

Proof