This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) = 𝑌 )