Theorem lspdisj

Description: The span of a vector not in a subspace is disjoint with the subspace. (Contributed by NM, 6-Apr-2015)

	Ref	Expression
Hypotheses	lspdisj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspdisj.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lspdisj.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspdisj.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspdisj.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspdisj.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lspdisj.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspdisj.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
Assertion	lspdisj	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } )

Proof

Step	Hyp	Ref	Expression
1		lspdisj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspdisj.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lspdisj.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspdisj.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5		lspdisj.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lspdisj.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		lspdisj.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8		lspdisj.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	5 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14	11 12 1 13 3	lspsnel	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
15	10 7 14	syl2anc	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
16	15	biimpa	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
17	16	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
18		simprr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
19	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ¬ 𝑋 ∈ 𝑈 )
20		simplr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑣 ∈ 𝑈 )
21	18 20	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
22		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
23	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑊 ∈ LVec )
24	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑈 ∈ 𝑆 )
25	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑋 ∈ 𝑉 )
26		simprl	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
27	1 13 11 12 22 4 23 24 25 26	lssvs0or	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 ↔ ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 ∈ 𝑈 ) ) )
28	21 27	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 ∈ 𝑈 ) )
29	28	orcomd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑋 ∈ 𝑈 ∨ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
30	29	ord	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( ¬ 𝑋 ∈ 𝑈 → 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
31	19 30	mpd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
32	31	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
33	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑊 ∈ LMod )
34	1 11 13 22 2	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
35	33 25 34	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
36	18 32 35	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ) → 𝑣 = 0 )
37	36	exp32	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → 𝑣 = 0 ) ) )
38	37	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → 𝑣 = 0 ) ) )
39	38	rexlimdv	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑣 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → 𝑣 = 0 ) )
40	17 39	mpd	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑣 = 0 )
41	40	ex	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 = 0 ) )
42		elin	⊢ ( 𝑣 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) ↔ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑣 ∈ 𝑈 ) )
43		velsn	⊢ ( 𝑣 ∈ { 0 } ↔ 𝑣 = 0 )
44	41 42 43	3imtr4g	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) → 𝑣 ∈ { 0 } ) )
45	44	ssrdv	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) ⊆ { 0 } )
46	1 4 3	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
47	10 7 46	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
48	2 4	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 ) → { 0 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
49	10 47 48	syl2anc	⊢ ( 𝜑 → { 0 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
50	2 4	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → { 0 } ⊆ 𝑈 )
51	10 6 50	syl2anc	⊢ ( 𝜑 → { 0 } ⊆ 𝑈 )
52	49 51	ssind	⊢ ( 𝜑 → { 0 } ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) )
53	45 52	eqssd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ 𝑈 ) = { 0 } )