Theorem lvecvs0or

Description: If a scalar product is zero, one of its factors must be zero. ( hvmul0or analog.) (Contributed by NM, 2-Jul-2014)

	Ref	Expression
Hypotheses	lvecmul0or.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lvecmul0or.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lvecmul0or.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lvecmul0or.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lvecmul0or.o	⊢ 𝑂 = ( 0g ‘ 𝐹 )
	lvecmul0or.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lvecmul0or.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lvecmul0or.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	lvecmul0or.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lvecvs0or	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lvecmul0or.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lvecmul0or.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		lvecmul0or.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lvecmul0or.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lvecmul0or.o	⊢ 𝑂 = ( 0g ‘ 𝐹 )
6		lvecmul0or.z	⊢ 0 = ( 0g ‘ 𝑊 )
7		lvecmul0or.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		lvecmul0or.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9		lvecmul0or.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		df-ne	⊢ ( 𝐴 ≠ 𝑂 ↔ ¬ 𝐴 = 𝑂 )
11		oveq2	⊢ ( ( 𝐴 · 𝑋 ) = 0 → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) )
12	11	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) )
13	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝑊 ∈ LVec )
14	3	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
15	13 14	syl	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝐹 ∈ DivRing )
16	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝐴 ∈ 𝐾 )
17		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝐴 ≠ 𝑂 )
18		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
19		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
20		eqid	⊢ ( invr ‘ 𝐹 ) = ( invr ‘ 𝐹 )
21	4 5 18 19 20	drnginvrl	⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
22	15 16 17 21	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
23	22	oveq1d	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( 1r ‘ 𝐹 ) · 𝑋 ) )
24		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25	7 24	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝑊 ∈ LMod )
27	4 5 20	drnginvrcl	⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 𝑂 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
28	15 16 17 27	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
29	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝑋 ∈ 𝑉 )
30	1 3 2 4 18	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
31	26 28 16 29 30	syl13anc	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
32	1 3 2 19	lmodvs1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
33	25 9 32	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
35	23 31 34	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = 𝑋 )
36	35	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = 𝑋 )
37	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → 𝑊 ∈ LMod )
38	37	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → 𝑊 ∈ LMod )
39	28	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
40	3 2 4 6	lmodvs0	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) = 0 )
41	38 39 40	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) = 0 )
42	12 36 41	3eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → 𝑋 = 0 )
43	42	ex	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → ( 𝐴 ≠ 𝑂 → 𝑋 = 0 ) )
44	10 43	biimtrrid	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → ( ¬ 𝐴 = 𝑂 → 𝑋 = 0 ) )
45	44	orrd	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) )
46	45	ex	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 → ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )
47	1 3 2 5 6	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑂 · 𝑋 ) = 0 )
48	25 9 47	syl2anc	⊢ ( 𝜑 → ( 𝑂 · 𝑋 ) = 0 )
49		oveq1	⊢ ( 𝐴 = 𝑂 → ( 𝐴 · 𝑋 ) = ( 𝑂 · 𝑋 ) )
50	49	eqeq1d	⊢ ( 𝐴 = 𝑂 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝑂 · 𝑋 ) = 0 ) )
51	48 50	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = 𝑂 → ( 𝐴 · 𝑋 ) = 0 ) )
52	3 2 4 6	lmodvs0	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 · 0 ) = 0 )
53	25 8 52	syl2anc	⊢ ( 𝜑 → ( 𝐴 · 0 ) = 0 )
54		oveq2	⊢ ( 𝑋 = 0 → ( 𝐴 · 𝑋 ) = ( 𝐴 · 0 ) )
55	54	eqeq1d	⊢ ( 𝑋 = 0 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) )
56	53 55	syl5ibrcom	⊢ ( 𝜑 → ( 𝑋 = 0 → ( 𝐴 · 𝑋 ) = 0 ) )
57	51 56	jaod	⊢ ( 𝜑 → ( ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) → ( 𝐴 · 𝑋 ) = 0 ) )
58	46 57	impbid	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )