Theorem cvsmuleqdivd

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$$
	cvsmuleqdivd.1	$$⊢\phi \to A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}Y$$
Assertion	cvsmuleqdivd	$$⊢\phi \to X=\left(\frac{B}{A}\right)\underset{\dot{}}{·}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		cvsmuleqdivd.1	$$⊢\phi \to A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}Y$$
12	11	oveq2d	$$⊢\phi \to \left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)=\left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(B\underset{\dot{}}{·}Y\right)$$
13	5	cvsclm	$$⊢\phi \to W\in \mathrm{CMod}$$
14	3 4	clmsscn	$$⊢W\in \mathrm{CMod}\to K\subseteq ℂ$$
15	13 14	syl	$$⊢\phi \to K\subseteq ℂ$$
16	15 6	sseldd	$$⊢\phi \to A\in ℂ$$
17	16 10	recid2d	$$⊢\phi \to \left(\frac{1}{A}\right)A=1$$
18	17	oveq1d	$$⊢\phi \to \left(\frac{1}{A}\right)A\underset{\dot{}}{·}X=1\underset{\dot{}}{·}X$$
19	3	clm1	$$⊢W\in \mathrm{CMod}\to 1=1_F$$
20	13 19	syl	$$⊢\phi \to 1=1_F$$
21	3	clmring	$$⊢W\in \mathrm{CMod}\to F\in \mathrm{Ring}$$
22		eqid	$$⊢1_F=1_F$$
23	4 22	ringidcl	$$⊢F\in \mathrm{Ring}\to 1_F\in K$$
24	13 21 23	3syl	$$⊢\phi \to 1_F\in K$$
25	20 24	eqeltrd	$$⊢\phi \to 1\in K$$
26	3 4	cvsdivcl	$$⊢\left(W\in \mathrm{ℂVec}\wedge \left(1\in K\wedge A\in K\wedge A\ne 0\right)\right)\to \frac{1}{A}\in K$$
27	5 25 6 10 26	syl13anc	$$⊢\phi \to \frac{1}{A}\in K$$
28	1 3 2 4	clmvsass	$$⊢\left(W\in \mathrm{CMod}\wedge \left(\frac{1}{A}\in K\wedge A\in K\wedge X\in V\right)\right)\to \left(\frac{1}{A}\right)A\underset{\dot{}}{·}X=\left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)$$
29	13 27 6 8 28	syl13anc	$$⊢\phi \to \left(\frac{1}{A}\right)A\underset{\dot{}}{·}X=\left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)$$
30	1 2	clmvs1	$$⊢\left(W\in \mathrm{CMod}\wedge X\in V\right)\to 1\underset{\dot{}}{·}X=X$$
31	13 8 30	syl2anc	$$⊢\phi \to 1\underset{\dot{}}{·}X=X$$
32	18 29 31	3eqtr3d	$$⊢\phi \to \left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)=X$$
33	15 7	sseldd	$$⊢\phi \to B\in ℂ$$
34	33 16 10	divrec2d	$$⊢\phi \to \frac{B}{A}=\left(\frac{1}{A}\right)B$$
35	34	oveq1d	$$⊢\phi \to \left(\frac{B}{A}\right)\underset{\dot{}}{·}Y=\left(\frac{1}{A}\right)B\underset{\dot{}}{·}Y$$
36	1 3 2 4	clmvsass	$$⊢\left(W\in \mathrm{CMod}\wedge \left(\frac{1}{A}\in K\wedge B\in K\wedge Y\in V\right)\right)\to \left(\frac{1}{A}\right)B\underset{\dot{}}{·}Y=\left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(B\underset{\dot{}}{·}Y\right)$$
37	13 27 7 9 36	syl13anc	$$⊢\phi \to \left(\frac{1}{A}\right)B\underset{\dot{}}{·}Y=\left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(B\underset{\dot{}}{·}Y\right)$$
38	35 37	eqtr2d	$$⊢\phi \to \left(\frac{1}{A}\right)\underset{\dot{}}{·}\left(B\underset{\dot{}}{·}Y\right)=\left(\frac{B}{A}\right)\underset{\dot{}}{·}Y$$
39	12 32 38	3eqtr3d	$$⊢\phi \to X=\left(\frac{B}{A}\right)\underset{\dot{}}{·}Y$$