Metamath Proof Explorer


Theorem lvecinv

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

Ref Expression
Hypotheses lvecinv.v V = Base W
lvecinv.t · ˙ = W
lvecinv.f F = Scalar W
lvecinv.k K = Base F
lvecinv.o 0 ˙ = 0 F
lvecinv.i I = inv r F
lvecinv.w φ W LVec
lvecinv.a φ A K 0 ˙
lvecinv.x φ X V
lvecinv.y φ Y V
Assertion lvecinv φ X = A · ˙ Y Y = I A · ˙ X

Proof

Step Hyp Ref Expression
1 lvecinv.v V = Base W
2 lvecinv.t · ˙ = W
3 lvecinv.f F = Scalar W
4 lvecinv.k K = Base F
5 lvecinv.o 0 ˙ = 0 F
6 lvecinv.i I = inv r F
7 lvecinv.w φ W LVec
8 lvecinv.a φ A K 0 ˙
9 lvecinv.x φ X V
10 lvecinv.y φ Y V
11 oveq2 X = A · ˙ Y I A · ˙ X = I A · ˙ A · ˙ Y
12 3 lvecdrng W LVec F DivRing
13 7 12 syl φ F DivRing
14 8 eldifad φ A K
15 eldifsni A K 0 ˙ A 0 ˙
16 8 15 syl φ A 0 ˙
17 eqid F = F
18 eqid 1 F = 1 F
19 4 5 17 18 6 drnginvrl F DivRing A K A 0 ˙ I A F A = 1 F
20 13 14 16 19 syl3anc φ I A F A = 1 F
21 20 oveq1d φ I A F A · ˙ Y = 1 F · ˙ Y
22 lveclmod W LVec W LMod
23 7 22 syl φ W LMod
24 4 5 6 drnginvrcl F DivRing A K A 0 ˙ I A K
25 13 14 16 24 syl3anc φ I A K
26 1 3 2 4 17 lmodvsass W LMod I A K A K Y V I A F A · ˙ Y = I A · ˙ A · ˙ Y
27 23 25 14 10 26 syl13anc φ I A F A · ˙ Y = I A · ˙ A · ˙ Y
28 1 3 2 18 lmodvs1 W LMod Y V 1 F · ˙ Y = Y
29 23 10 28 syl2anc φ 1 F · ˙ Y = Y
30 21 27 29 3eqtr3d φ I A · ˙ A · ˙ Y = Y
31 11 30 sylan9eqr φ X = A · ˙ Y I A · ˙ X = Y
32 4 5 17 18 6 drnginvrr F DivRing A K A 0 ˙ A F I A = 1 F
33 13 14 16 32 syl3anc φ A F I A = 1 F
34 33 oveq1d φ A F I A · ˙ X = 1 F · ˙ X
35 1 3 2 4 17 lmodvsass W LMod A K I A K X V A F I A · ˙ X = A · ˙ I A · ˙ X
36 23 14 25 9 35 syl13anc φ A F I A · ˙ X = A · ˙ I A · ˙ X
37 1 3 2 18 lmodvs1 W LMod X V 1 F · ˙ X = X
38 23 9 37 syl2anc φ 1 F · ˙ X = X
39 34 36 38 3eqtr3rd φ X = A · ˙ I A · ˙ X
40 oveq2 I A · ˙ X = Y A · ˙ I A · ˙ X = A · ˙ Y
41 39 40 sylan9eq φ I A · ˙ X = Y X = A · ˙ Y
42 31 41 impbida φ X = A · ˙ Y I A · ˙ X = Y
43 eqcom I A · ˙ X = Y Y = I A · ˙ X
44 42 43 bitrdi φ X = A · ˙ Y Y = I A · ˙ X