Theorem lvecinv

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

	Ref	Expression
Hypotheses	lvecinv.v	$$⊢V={\mathrm{Base}}_W$$
	lvecinv.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lvecinv.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lvecinv.k	$$⊢K={\mathrm{Base}}_F$$
	lvecinv.o	$$⊢\underset{\dot{}}{0}=0_F$$
	lvecinv.i	$$⊢I={inv}_r\left(F\right)$$
	lvecinv.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lvecinv.a	$$⊢\phi \to A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lvecinv.x	$$⊢\phi \to X\in V$$
	lvecinv.y	$$⊢\phi \to Y\in V$$
Assertion	lvecinv	$$⊢\phi \to \left(X=A\underset{\dot{}}{·}Y\leftrightarrow Y=I\left(A\right)\underset{\dot{}}{·}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lvecinv.v	$$⊢V={\mathrm{Base}}_W$$
2		lvecinv.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lvecinv.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lvecinv.k	$$⊢K={\mathrm{Base}}_F$$
5		lvecinv.o	$$⊢\underset{\dot{}}{0}=0_F$$
6		lvecinv.i	$$⊢I={inv}_r\left(F\right)$$
7		lvecinv.w	$$⊢\phi \to W\in \mathrm{LVec}$$
8		lvecinv.a	$$⊢\phi \to A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9		lvecinv.x	$$⊢\phi \to X\in V$$
10		lvecinv.y	$$⊢\phi \to Y\in V$$
11		oveq2	$$⊢X=A\underset{\dot{}}{·}Y\to I\left(A\right)\underset{\dot{}}{·}X=I\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)$$
12	3	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
13	7 12	syl	$$⊢\phi \to F\in \mathrm{DivRing}$$
14	8	eldifad	$$⊢\phi \to A\in K$$
15		eldifsni	$$⊢A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to A\ne \underset{\dot{}}{0}$$
16	8 15	syl	$$⊢\phi \to A\ne \underset{\dot{}}{0}$$
17		eqid	$$⊢{\cdot }_F={\cdot }_F$$
18		eqid	$$⊢1_F=1_F$$
19	4 5 17 18 6	drnginvrl	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne \underset{\dot{}}{0}\right)\to I\left(A\right){\cdot }_{F}A=1_F$$
20	13 14 16 19	syl3anc	$$⊢\phi \to I\left(A\right){\cdot }_{F}A=1_F$$
21	20	oveq1d	$$⊢\phi \to \left(I\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}Y=1_F\underset{\dot{}}{·}Y$$
22		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
23	7 22	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
24	4 5 6	drnginvrcl	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne \underset{\dot{}}{0}\right)\to I\left(A\right)\in K$$
25	13 14 16 24	syl3anc	$$⊢\phi \to I\left(A\right)\in K$$
26	1 3 2 4 17	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(I\left(A\right)\in K\wedge A\in K\wedge Y\in V\right)\right)\to \left(I\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}Y=I\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)$$
27	23 25 14 10 26	syl13anc	$$⊢\phi \to \left(I\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}Y=I\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)$$
28	1 3 2 18	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\right)\to 1_F\underset{\dot{}}{·}Y=Y$$
29	23 10 28	syl2anc	$$⊢\phi \to 1_F\underset{\dot{}}{·}Y=Y$$
30	21 27 29	3eqtr3d	$$⊢\phi \to I\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)=Y$$
31	11 30	sylan9eqr	$$⊢\left(\phi \wedge X=A\underset{\dot{}}{·}Y\right)\to I\left(A\right)\underset{\dot{}}{·}X=Y$$
32	4 5 17 18 6	drnginvrr	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne \underset{\dot{}}{0}\right)\to A{\cdot }_{F}I\left(A\right)=1_F$$
33	13 14 16 32	syl3anc	$$⊢\phi \to A{\cdot }_{F}I\left(A\right)=1_F$$
34	33	oveq1d	$$⊢\phi \to \left(A{\cdot }_{F}I\left(A\right)\right)\underset{\dot{}}{·}X=1_F\underset{\dot{}}{·}X$$
35	1 3 2 4 17	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(A\in K\wedge I\left(A\right)\in K\wedge X\in V\right)\right)\to \left(A{\cdot }_{F}I\left(A\right)\right)\underset{\dot{}}{·}X=A\underset{\dot{}}{·}\left(I\left(A\right)\underset{\dot{}}{·}X\right)$$
36	23 14 25 9 35	syl13anc	$$⊢\phi \to \left(A{\cdot }_{F}I\left(A\right)\right)\underset{\dot{}}{·}X=A\underset{\dot{}}{·}\left(I\left(A\right)\underset{\dot{}}{·}X\right)$$
37	1 3 2 18	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to 1_F\underset{\dot{}}{·}X=X$$
38	23 9 37	syl2anc	$$⊢\phi \to 1_F\underset{\dot{}}{·}X=X$$
39	34 36 38	3eqtr3rd	$$⊢\phi \to X=A\underset{\dot{}}{·}\left(I\left(A\right)\underset{\dot{}}{·}X\right)$$
40		oveq2	$$⊢I\left(A\right)\underset{\dot{}}{·}X=Y\to A\underset{\dot{}}{·}\left(I\left(A\right)\underset{\dot{}}{·}X\right)=A\underset{\dot{}}{·}Y$$
41	39 40	sylan9eq	$$⊢\left(\phi \wedge I\left(A\right)\underset{\dot{}}{·}X=Y\right)\to X=A\underset{\dot{}}{·}Y$$
42	31 41	impbida	$$⊢\phi \to \left(X=A\underset{\dot{}}{·}Y\leftrightarrow I\left(A\right)\underset{\dot{}}{·}X=Y\right)$$
43		eqcom	$$⊢I\left(A\right)\underset{\dot{}}{·}X=Y\leftrightarrow Y=I\left(A\right)\underset{\dot{}}{·}X$$
44	42 43	bitrdi	$$⊢\phi \to \left(X=A\underset{\dot{}}{·}Y\leftrightarrow Y=I\left(A\right)\underset{\dot{}}{·}X\right)$$