lspdisj2

Description: Unequal spans are disjoint (share only the zero vector). (Contributed by NM, 22-Mar-2015)

	Ref	Expression
Hypotheses	lspdisj2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspdisj2.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	lspdisj2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspdisj2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspdisj2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspdisj2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspdisj2.q	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion	lspdisj2	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )

Proof

Step	Hyp	Ref	Expression
1		lspdisj2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspdisj2.o	⊢ 0 = ( 0_g ‘ 𝑊 )
3		lspdisj2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspdisj2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lspdisj2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lspdisj2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7		lspdisj2.q	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
8		sneq	⊢ ( 𝑋 = 0 → { 𝑋 } = { 0 } )
9	8	fveq2d	⊢ ( 𝑋 = 0 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 0 } ) )
10		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	4 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12	2 3	lspsn0	⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
13	11 12	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { 0 } ) = { 0 } )
14	9 13	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = { 0 } )
15	14	ineq1d	⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) )
16		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
17	1 16 3	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
18	11 6 17	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
19	2 16	lss0ss	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → { 0 } ⊆ ( 𝑁 ‘ { 𝑌 } ) )
20	11 18 19	syl2anc	⊢ ( 𝜑 → { 0 } ⊆ ( 𝑁 ‘ { 𝑌 } ) )
21		df-ss	⊢ ( { 0 } ⊆ ( 𝑁 ‘ { 𝑌 } ) ↔ ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
22	20 21	sylib	⊢ ( 𝜑 → ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( { 0 } ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
24	15 23	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
25	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LVec )
26	18	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
27	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉 )
28	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
29	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LVec )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ 𝑉 )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑌 ∈ 𝑉 )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
33		simplr	⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ≠ 0 )
34	1 2 3 29 31 32 33	lspsneleq	⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ 0 ) ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
35	34	ex	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
36	35	necon3ad	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
37	28 36	mpd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
38	1 2 3 16 25 26 27 37	lspdisj	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )
39	24 38	pm2.61dane	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∩ ( 𝑁 ‘ { 𝑌 } ) ) = { 0 } )

Metamath Proof Explorer

Theorem lspdisj2

Proof