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 ⊢ ( 𝜑 → ( 𝑋 = ( 𝐴 · 𝑌 ) ↔ 𝑌 = ( ( 𝐼 ‘ 𝐴 ) · 𝑋 ) ) )