Theorem cvsmuleqdivd

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

	Ref	Expression
Hypotheses	cvsdiveqd.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cvsdiveqd.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	cvsdiveqd.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cvsdiveqd.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	cvsdiveqd.w	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
	cvsdiveqd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	cvsdiveqd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
	cvsdiveqd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	cvsdiveqd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	cvsdiveqd.1	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	cvsmuleqdivd.1	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑌 ) )
Assertion	cvsmuleqdivd	⊢ ( 𝜑 → 𝑋 = ( ( 𝐵 / 𝐴 ) · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cvsdiveqd.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		cvsdiveqd.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		cvsdiveqd.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		cvsdiveqd.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		cvsdiveqd.w	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
6		cvsdiveqd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
7		cvsdiveqd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
8		cvsdiveqd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		cvsdiveqd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10		cvsdiveqd.1	⊢ ( 𝜑 → 𝐴 ≠ 0 )
11		cvsmuleqdivd.1	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑌 ) )
12	11	oveq2d	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) · ( 𝐴 · 𝑋 ) ) = ( ( 1 / 𝐴 ) · ( 𝐵 · 𝑌 ) ) )
13	5	cvsclm	⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
14	3 4	clmsscn	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
15	13 14	syl	⊢ ( 𝜑 → 𝐾 ⊆ ℂ )
16	15 6	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
17	16 10	recid2d	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )
18	17	oveq1d	⊢ ( 𝜑 → ( ( ( 1 / 𝐴 ) · 𝐴 ) · 𝑋 ) = ( 1 · 𝑋 ) )
19	3	clm1	⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ 𝐹 ) )
20	13 19	syl	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝐹 ) )
21	3	clmring	⊢ ( 𝑊 ∈ ℂMod → 𝐹 ∈ Ring )
22		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
23	4 22	ringidcl	⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
24	13 21 23	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
25	20 24	eqeltrd	⊢ ( 𝜑 → 1 ∈ 𝐾 )
26	3 4	cvsdivcl	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 1 ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) ) → ( 1 / 𝐴 ) ∈ 𝐾 )
27	5 25 6 10 26	syl13anc	⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ 𝐾 )
28	1 3 2 4	clmvsass	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( ( 1 / 𝐴 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 1 / 𝐴 ) · 𝐴 ) · 𝑋 ) = ( ( 1 / 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
29	13 27 6 8 28	syl13anc	⊢ ( 𝜑 → ( ( ( 1 / 𝐴 ) · 𝐴 ) · 𝑋 ) = ( ( 1 / 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
30	1 2	clmvs1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( 1 · 𝑋 ) = 𝑋 )
31	13 8 30	syl2anc	⊢ ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )
32	18 29 31	3eqtr3d	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) · ( 𝐴 · 𝑋 ) ) = 𝑋 )
33	15 7	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
34	33 16 10	divrec2d	⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝐵 ) )
35	34	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑌 ) = ( ( ( 1 / 𝐴 ) · 𝐵 ) · 𝑌 ) )
36	1 3 2 4	clmvsass	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( ( 1 / 𝐴 ) ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 1 / 𝐴 ) · 𝐵 ) · 𝑌 ) = ( ( 1 / 𝐴 ) · ( 𝐵 · 𝑌 ) ) )
37	13 27 7 9 36	syl13anc	⊢ ( 𝜑 → ( ( ( 1 / 𝐴 ) · 𝐵 ) · 𝑌 ) = ( ( 1 / 𝐴 ) · ( 𝐵 · 𝑌 ) ) )
38	35 37	eqtr2d	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) · ( 𝐵 · 𝑌 ) ) = ( ( 𝐵 / 𝐴 ) · 𝑌 ) )
39	12 32 38	3eqtr3d	⊢ ( 𝜑 → 𝑋 = ( ( 𝐵 / 𝐴 ) · 𝑌 ) )