Theorem cvsdiveqd

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

	Ref	Expression
Hypotheses	cvsdiveqd.v	$$⊢V={\mathrm{Base}}_W$$
	cvsdiveqd.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	cvsdiveqd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cvsdiveqd.k	$$⊢K={\mathrm{Base}}_F$$
	cvsdiveqd.w	$$⊢\phi \to W\in \mathrm{ℂVec}$$
	cvsdiveqd.a	$$⊢\phi \to A\in K$$
	cvsdiveqd.b	$$⊢\phi \to B\in K$$
	cvsdiveqd.x	$$⊢\phi \to X\in V$$
	cvsdiveqd.y	$$⊢\phi \to Y\in V$$
	cvsdiveqd.1	$$⊢\phi \to A\ne 0$$
	cvsdiveqd.2	$$⊢\phi \to B\ne 0$$
	cvsdiveqd.3	$$⊢\phi \to X=\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y$$
Assertion	cvsdiveqd	$$⊢\phi \to \left(\frac{B}{A}\right)\underset{\dot{}}{·}X=Y$$

Proof

Step	Hyp	Ref	Expression
1		cvsdiveqd.v	$$⊢V={\mathrm{Base}}_W$$
2		cvsdiveqd.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		cvsdiveqd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		cvsdiveqd.k	$$⊢K={\mathrm{Base}}_F$$
5		cvsdiveqd.w	$$⊢\phi \to W\in \mathrm{ℂVec}$$
6		cvsdiveqd.a	$$⊢\phi \to A\in K$$
7		cvsdiveqd.b	$$⊢\phi \to B\in K$$
8		cvsdiveqd.x	$$⊢\phi \to X\in V$$
9		cvsdiveqd.y	$$⊢\phi \to Y\in V$$
10		cvsdiveqd.1	$$⊢\phi \to A\ne 0$$
11		cvsdiveqd.2	$$⊢\phi \to B\ne 0$$
12		cvsdiveqd.3	$$⊢\phi \to X=\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y$$
13	12	oveq2d	$$⊢\phi \to \left(\frac{B}{A}\right)\underset{\dot{}}{·}X=\left(\frac{B}{A}\right)\underset{\dot{}}{·}\left(\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y\right)$$
14	5	cvsclm	$$⊢\phi \to W\in \mathrm{CMod}$$
15	3 4	clmsscn	$$⊢W\in \mathrm{CMod}\to K\subseteq ℂ$$
16	14 15	syl	$$⊢\phi \to K\subseteq ℂ$$
17	16 7	sseldd	$$⊢\phi \to B\in ℂ$$
18	16 6	sseldd	$$⊢\phi \to A\in ℂ$$
19	17 18 11 10	divcan6d	$$⊢\phi \to \left(\frac{B}{A}\right)\left(\frac{A}{B}\right)=1$$
20	19	oveq1d	$$⊢\phi \to \left(\frac{B}{A}\right)\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y=1\underset{\dot{}}{·}Y$$
21	3 4	cvsdivcl	$$⊢\left(W\in \mathrm{ℂVec}\wedge \left(B\in K\wedge A\in K\wedge A\ne 0\right)\right)\to \frac{B}{A}\in K$$
22	5 7 6 10 21	syl13anc	$$⊢\phi \to \frac{B}{A}\in K$$
23	3 4	cvsdivcl	$$⊢\left(W\in \mathrm{ℂVec}\wedge \left(A\in K\wedge B\in K\wedge B\ne 0\right)\right)\to \frac{A}{B}\in K$$
24	5 6 7 11 23	syl13anc	$$⊢\phi \to \frac{A}{B}\in K$$
25	1 3 2 4	clmvsass	$$⊢\left(W\in \mathrm{CMod}\wedge \left(\frac{B}{A}\in K\wedge \frac{A}{B}\in K\wedge Y\in V\right)\right)\to \left(\frac{B}{A}\right)\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y=\left(\frac{B}{A}\right)\underset{\dot{}}{·}\left(\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y\right)$$
26	14 22 24 9 25	syl13anc	$$⊢\phi \to \left(\frac{B}{A}\right)\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y=\left(\frac{B}{A}\right)\underset{\dot{}}{·}\left(\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y\right)$$
27	1 2	clmvs1	$$⊢\left(W\in \mathrm{CMod}\wedge Y\in V\right)\to 1\underset{\dot{}}{·}Y=Y$$
28	14 9 27	syl2anc	$$⊢\phi \to 1\underset{\dot{}}{·}Y=Y$$
29	20 26 28	3eqtr3d	$$⊢\phi \to \left(\frac{B}{A}\right)\underset{\dot{}}{·}\left(\left(\frac{A}{B}\right)\underset{\dot{}}{·}Y\right)=Y$$
30	13 29	eqtrd	$$⊢\phi \to \left(\frac{B}{A}\right)\underset{\dot{}}{·}X=Y$$