Metamath Proof Explorer


Theorem lvecinv

Description: Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015)

Ref Expression
Hypotheses lvecinv.v 𝑉 = ( Base ‘ 𝑊 )
lvecinv.t · = ( ·𝑠𝑊 )
lvecinv.f 𝐹 = ( Scalar ‘ 𝑊 )
lvecinv.k 𝐾 = ( Base ‘ 𝐹 )
lvecinv.o 0 = ( 0g𝐹 )
lvecinv.i 𝐼 = ( invr𝐹 )
lvecinv.w ( 𝜑𝑊 ∈ LVec )
lvecinv.a ( 𝜑𝐴 ∈ ( 𝐾 ∖ { 0 } ) )
lvecinv.x ( 𝜑𝑋𝑉 )
lvecinv.y ( 𝜑𝑌𝑉 )
Assertion lvecinv ( 𝜑 → ( 𝑋 = ( 𝐴 · 𝑌 ) ↔ 𝑌 = ( ( 𝐼𝐴 ) · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 lvecinv.v 𝑉 = ( Base ‘ 𝑊 )
2 lvecinv.t · = ( ·𝑠𝑊 )
3 lvecinv.f 𝐹 = ( Scalar ‘ 𝑊 )
4 lvecinv.k 𝐾 = ( Base ‘ 𝐹 )
5 lvecinv.o 0 = ( 0g𝐹 )
6 lvecinv.i 𝐼 = ( invr𝐹 )
7 lvecinv.w ( 𝜑𝑊 ∈ LVec )
8 lvecinv.a ( 𝜑𝐴 ∈ ( 𝐾 ∖ { 0 } ) )
9 lvecinv.x ( 𝜑𝑋𝑉 )
10 lvecinv.y ( 𝜑𝑌𝑉 )
11 oveq2 ( 𝑋 = ( 𝐴 · 𝑌 ) → ( ( 𝐼𝐴 ) · 𝑋 ) = ( ( 𝐼𝐴 ) · ( 𝐴 · 𝑌 ) ) )
12 3 lvecdrng ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
13 7 12 syl ( 𝜑𝐹 ∈ DivRing )
14 8 eldifad ( 𝜑𝐴𝐾 )
15 eldifsni ( 𝐴 ∈ ( 𝐾 ∖ { 0 } ) → 𝐴0 )
16 8 15 syl ( 𝜑𝐴0 )
17 eqid ( .r𝐹 ) = ( .r𝐹 )
18 eqid ( 1r𝐹 ) = ( 1r𝐹 )
19 4 5 17 18 6 drnginvrl ( ( 𝐹 ∈ DivRing ∧ 𝐴𝐾𝐴0 ) → ( ( 𝐼𝐴 ) ( .r𝐹 ) 𝐴 ) = ( 1r𝐹 ) )
20 13 14 16 19 syl3anc ( 𝜑 → ( ( 𝐼𝐴 ) ( .r𝐹 ) 𝐴 ) = ( 1r𝐹 ) )
21 20 oveq1d ( 𝜑 → ( ( ( 𝐼𝐴 ) ( .r𝐹 ) 𝐴 ) · 𝑌 ) = ( ( 1r𝐹 ) · 𝑌 ) )
22 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
23 7 22 syl ( 𝜑𝑊 ∈ LMod )
24 4 5 6 drnginvrcl ( ( 𝐹 ∈ DivRing ∧ 𝐴𝐾𝐴0 ) → ( 𝐼𝐴 ) ∈ 𝐾 )
25 13 14 16 24 syl3anc ( 𝜑 → ( 𝐼𝐴 ) ∈ 𝐾 )
26 1 3 2 4 17 lmodvsass ( ( 𝑊 ∈ LMod ∧ ( ( 𝐼𝐴 ) ∈ 𝐾𝐴𝐾𝑌𝑉 ) ) → ( ( ( 𝐼𝐴 ) ( .r𝐹 ) 𝐴 ) · 𝑌 ) = ( ( 𝐼𝐴 ) · ( 𝐴 · 𝑌 ) ) )
27 23 25 14 10 26 syl13anc ( 𝜑 → ( ( ( 𝐼𝐴 ) ( .r𝐹 ) 𝐴 ) · 𝑌 ) = ( ( 𝐼𝐴 ) · ( 𝐴 · 𝑌 ) ) )
28 1 3 2 18 lmodvs1 ( ( 𝑊 ∈ LMod ∧ 𝑌𝑉 ) → ( ( 1r𝐹 ) · 𝑌 ) = 𝑌 )
29 23 10 28 syl2anc ( 𝜑 → ( ( 1r𝐹 ) · 𝑌 ) = 𝑌 )
30 21 27 29 3eqtr3d ( 𝜑 → ( ( 𝐼𝐴 ) · ( 𝐴 · 𝑌 ) ) = 𝑌 )
31 11 30 sylan9eqr ( ( 𝜑𝑋 = ( 𝐴 · 𝑌 ) ) → ( ( 𝐼𝐴 ) · 𝑋 ) = 𝑌 )
32 4 5 17 18 6 drnginvrr ( ( 𝐹 ∈ DivRing ∧ 𝐴𝐾𝐴0 ) → ( 𝐴 ( .r𝐹 ) ( 𝐼𝐴 ) ) = ( 1r𝐹 ) )
33 13 14 16 32 syl3anc ( 𝜑 → ( 𝐴 ( .r𝐹 ) ( 𝐼𝐴 ) ) = ( 1r𝐹 ) )
34 33 oveq1d ( 𝜑 → ( ( 𝐴 ( .r𝐹 ) ( 𝐼𝐴 ) ) · 𝑋 ) = ( ( 1r𝐹 ) · 𝑋 ) )
35 1 3 2 4 17 lmodvsass ( ( 𝑊 ∈ LMod ∧ ( 𝐴𝐾 ∧ ( 𝐼𝐴 ) ∈ 𝐾𝑋𝑉 ) ) → ( ( 𝐴 ( .r𝐹 ) ( 𝐼𝐴 ) ) · 𝑋 ) = ( 𝐴 · ( ( 𝐼𝐴 ) · 𝑋 ) ) )
36 23 14 25 9 35 syl13anc ( 𝜑 → ( ( 𝐴 ( .r𝐹 ) ( 𝐼𝐴 ) ) · 𝑋 ) = ( 𝐴 · ( ( 𝐼𝐴 ) · 𝑋 ) ) )
37 1 3 2 18 lmodvs1 ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( ( 1r𝐹 ) · 𝑋 ) = 𝑋 )
38 23 9 37 syl2anc ( 𝜑 → ( ( 1r𝐹 ) · 𝑋 ) = 𝑋 )
39 34 36 38 3eqtr3rd ( 𝜑𝑋 = ( 𝐴 · ( ( 𝐼𝐴 ) · 𝑋 ) ) )
40 oveq2 ( ( ( 𝐼𝐴 ) · 𝑋 ) = 𝑌 → ( 𝐴 · ( ( 𝐼𝐴 ) · 𝑋 ) ) = ( 𝐴 · 𝑌 ) )
41 39 40 sylan9eq ( ( 𝜑 ∧ ( ( 𝐼𝐴 ) · 𝑋 ) = 𝑌 ) → 𝑋 = ( 𝐴 · 𝑌 ) )
42 31 41 impbida ( 𝜑 → ( 𝑋 = ( 𝐴 · 𝑌 ) ↔ ( ( 𝐼𝐴 ) · 𝑋 ) = 𝑌 ) )
43 eqcom ( ( ( 𝐼𝐴 ) · 𝑋 ) = 𝑌𝑌 = ( ( 𝐼𝐴 ) · 𝑋 ) )
44 42 43 bitrdi ( 𝜑 → ( 𝑋 = ( 𝐴 · 𝑌 ) ↔ 𝑌 = ( ( 𝐼𝐴 ) · 𝑋 ) ) )