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