Theorem mapdindp1

Description: Vector independence lemma. (Contributed by NM, 1-May-2015)

	Ref	Expression
Hypotheses	mapdindp1.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	mapdindp1.p	⊢ + = ( +g ‘ 𝑊 )
	mapdindp1.o	⊢ 0 = ( 0g ‘ 𝑊 )
	mapdindp1.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	mapdindp1.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	mapdindp1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	mapdindp1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	mapdindp1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
	mapdindp1.W	⊢ ( 𝜑 → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
	mapdindp1.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑍 } ) )
	mapdindp1.ne	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
	mapdindp1.f	⊢ ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
Assertion	mapdindp1	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		mapdindp1.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		mapdindp1.p	⊢ + = ( +g ‘ 𝑊 )
3		mapdindp1.o	⊢ 0 = ( 0g ‘ 𝑊 )
4		mapdindp1.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5		mapdindp1.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		mapdindp1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
7		mapdindp1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
8		mapdindp1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
9		mapdindp1.W	⊢ ( 𝜑 → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
10		mapdindp1.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑍 } ) )
11		mapdindp1.ne	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
12		mapdindp1.f	⊢ ( 𝜑 → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
13		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
14	6 13	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
15		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
16	5 15	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
17	3 4	lspsn0	⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
18	16 17	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { 0 } ) = { 0 } )
19	18	eqeq2d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 0 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )
20	6	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
21	1 3 4	lspsneq0	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
22	16 20 21	syl2anc	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
23	19 22	bitrd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 0 } ) ↔ 𝑋 = 0 ) )
24	23	necon3bid	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 0 } ) ↔ 𝑋 ≠ 0 ) )
25	14 24	mpbird	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 0 } ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 0 } ) )
27		sneq	⊢ ( ( 𝑌 + 𝑍 ) = 0 → { ( 𝑌 + 𝑍 ) } = { 0 } )
28	27	fveq2d	⊢ ( ( 𝑌 + 𝑍 ) = 0 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 0 } ) )
29	28	adantl	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 0 } ) )
30	26 29	neeqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) = 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
31	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
32	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑊 ∈ LVec )
33	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
34	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
35	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
36	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → 𝑤 ∈ ( 𝑉 ∖ { 0 } ) )
37	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑍 } ) )
38	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
39		simpr	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑌 + 𝑍 ) ≠ 0 )
40	1 2 3 4 32 33 34 35 36 37 31 38 39	mapdindp0	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
41	31 40	neeqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑌 + 𝑍 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
42	30 41	pm2.61dane	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )