cvsdiveqd

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 )
	cvsdiveqd.2	⊢ ( 𝜑 → 𝐵 ≠ 0 )
	cvsdiveqd.3	⊢ ( 𝜑 → 𝑋 = ( ( 𝐴 / 𝐵 ) · 𝑌 ) )
Assertion	cvsdiveqd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) = 𝑌 )

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		cvsdiveqd.2	⊢ ( 𝜑 → 𝐵 ≠ 0 )
12		cvsdiveqd.3	⊢ ( 𝜑 → 𝑋 = ( ( 𝐴 / 𝐵 ) · 𝑌 ) )
13	12	oveq2d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) = ( ( 𝐵 / 𝐴 ) · ( ( 𝐴 / 𝐵 ) · 𝑌 ) ) )
14	5	cvsclm	⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
15	3 4	clmsscn	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
16	14 15	syl	⊢ ( 𝜑 → 𝐾 ⊆ ℂ )
17	16 7	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
18	16 6	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
19	17 18 11 10	divcan6d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · ( 𝐴 / 𝐵 ) ) = 1 )
20	19	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐵 / 𝐴 ) · ( 𝐴 / 𝐵 ) ) · 𝑌 ) = ( 1 · 𝑌 ) )
21	3 4	cvsdivcl	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐵 ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) ) → ( 𝐵 / 𝐴 ) ∈ 𝐾 )
22	5 7 6 10 21	syl13anc	⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ 𝐾 )
23	3 4	cvsdivcl	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )
24	5 6 7 11 23	syl13anc	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) ∈ 𝐾 )
25	1 3 2 4	clmvsass	⊢ ( ( 𝑊 ∈ ℂMod ∧ ( ( 𝐵 / 𝐴 ) ∈ 𝐾 ∧ ( 𝐴 / 𝐵 ) ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝐵 / 𝐴 ) · ( 𝐴 / 𝐵 ) ) · 𝑌 ) = ( ( 𝐵 / 𝐴 ) · ( ( 𝐴 / 𝐵 ) · 𝑌 ) ) )
26	14 22 24 9 25	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐵 / 𝐴 ) · ( 𝐴 / 𝐵 ) ) · 𝑌 ) = ( ( 𝐵 / 𝐴 ) · ( ( 𝐴 / 𝐵 ) · 𝑌 ) ) )
27	1 2	clmvs1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑌 ∈ 𝑉 ) → ( 1 · 𝑌 ) = 𝑌 )
28	14 9 27	syl2anc	⊢ ( 𝜑 → ( 1 · 𝑌 ) = 𝑌 )
29	20 26 28	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · ( ( 𝐴 / 𝐵 ) · 𝑌 ) ) = 𝑌 )
30	13 29	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) = 𝑌 )

Metamath Proof Explorer

Theorem cvsdiveqd

Proof