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

Metamath Proof Explorer

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