Theorem lssvs0or

Description: If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015)

	Ref	Expression
Hypotheses	lssvs0or.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lssvs0or.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lssvs0or.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lssvs0or.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lssvs0or.o	⊢ 0 = ( 0g ‘ 𝐹 )
	lssvs0or.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssvs0or.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lssvs0or.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lssvs0or.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lssvs0or.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
Assertion	lssvs0or	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ∈ 𝑈 ↔ ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lssvs0or.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lssvs0or.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		lssvs0or.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lssvs0or.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lssvs0or.o	⊢ 0 = ( 0g ‘ 𝐹 )
6		lssvs0or.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
7		lssvs0or.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		lssvs0or.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
9		lssvs0or.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		lssvs0or.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
11	3	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
12	7 11	syl	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
13	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ DivRing )
14	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ 𝐾 )
15		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
16		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
17		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
18		eqid	⊢ ( invr ‘ 𝐹 ) = ( invr ‘ 𝐹 )
19	4 5 16 17 18	drnginvrl	⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
20	13 14 15 19	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
21	20	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( 1r ‘ 𝐹 ) · 𝑋 ) )
22		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
23	7 22	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
24	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑊 ∈ LMod )
25	4 5 18	drnginvrcl	⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
26	13 14 15 25	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
27	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑋 ∈ 𝑉 )
28	1 3 2 4 16	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
29	24 26 14 27 28	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
30	1 3 2 17	lmodvs1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
31	24 27 30	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
32	21 29 31	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑋 = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
33	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑈 ∈ 𝑆 )
34		simplr	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
35	3 2 4 6	lssvscl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) ∈ 𝑈 )
36	24 33 26 34 35	syl22anc	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) ∈ 𝑈 )
37	32 36	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑋 ∈ 𝑈 )
38	37	ex	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( 𝐴 ≠ 0 → 𝑋 ∈ 𝑈 ) )
39	38	necon1bd	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( ¬ 𝑋 ∈ 𝑈 → 𝐴 = 0 ) )
40	39	orrd	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( 𝑋 ∈ 𝑈 ∨ 𝐴 = 0 ) )
41	40	orcomd	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) )
42		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 · 𝑋 ) = ( 0 · 𝑋 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝐴 · 𝑋 ) = ( 0 · 𝑋 ) )
44		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
45	1 3 2 5 44	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝑊 ) )
46	23 9 45	syl2anc	⊢ ( 𝜑 → ( 0 · 𝑋 ) = ( 0g ‘ 𝑊 ) )
47	44 6	lss0cl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
48	23 8 47	syl2anc	⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
49	46 48	eqeltrd	⊢ ( 𝜑 → ( 0 · 𝑋 ) ∈ 𝑈 )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 0 · 𝑋 ) ∈ 𝑈 )
51	43 50	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
52	23	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LMod )
53	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
54	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐴 ∈ 𝐾 )
55		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
56	3 2 4 6	lssvscl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑈 ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
57	52 53 54 55 56	syl22anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
58	51 57	jaodan	⊢ ( ( 𝜑 ∧ ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
59	41 58	impbida	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ∈ 𝑈 ↔ ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) ) )