Theorem mapdindp4

Description: Vector independence lemma. (Contributed by NM, 29-Apr-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	mapdindp4	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑤 + 𝑌 ) } ) )

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		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14	5 13	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
15	9	eldifad	⊢ ( 𝜑 → 𝑤 ∈ 𝑉 )
16	7	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
17	1 2	lmodvacl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑤 + 𝑌 ) ∈ 𝑉 )
18	14 15 16 17	syl3anc	⊢ ( 𝜑 → ( 𝑤 + 𝑌 ) ∈ 𝑉 )
19	6	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
20	1 4 5 15 19 16 12	lspindpi	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
21	20	simprd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
22	21	necomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑤 } ) )
23	1 2 3 4 5 16 9 22	lspindp3	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { ( 𝑌 + 𝑤 ) } ) )
24	1 2	lmodcom	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑤 + 𝑌 ) = ( 𝑌 + 𝑤 ) )
25	14 15 16 24	syl3anc	⊢ ( 𝜑 → ( 𝑤 + 𝑌 ) = ( 𝑌 + 𝑤 ) )
26	25	sneqd	⊢ ( 𝜑 → { ( 𝑤 + 𝑌 ) } = { ( 𝑌 + 𝑤 ) } )
27	26	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) = ( 𝑁 ‘ { ( 𝑌 + 𝑤 ) } ) )
28	23 27	neeqtrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) )
29	10 28	eqnetrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ≠ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) )
30	1 3 4 5 6 16 15 11 12	lspindp1	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑤 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑤 , 𝑌 } ) ) )
31	30	simprd	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
32		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
33	8	eldifad	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
34	1 4 32 14 33 18	lsmpr	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 , ( 𝑤 + 𝑌 ) } ) = ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) )
35	1 2	lmodcom	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) → ( 𝑌 + 𝑤 ) = ( 𝑤 + 𝑌 ) )
36	14 16 15 35	syl3anc	⊢ ( 𝜑 → ( 𝑌 + 𝑤 ) = ( 𝑤 + 𝑌 ) )
37	36	preq2d	⊢ ( 𝜑 → { 𝑌 , ( 𝑌 + 𝑤 ) } = { 𝑌 , ( 𝑤 + 𝑌 ) } )
38	37	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , ( 𝑌 + 𝑤 ) } ) = ( 𝑁 ‘ { 𝑌 , ( 𝑤 + 𝑌 ) } ) )
39	1 2 4 14 16 15	lspprabs	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , ( 𝑌 + 𝑤 ) } ) = ( 𝑁 ‘ { 𝑌 , 𝑤 } ) )
40	1 4 32 14 16 18	lsmpr	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , ( 𝑤 + 𝑌 ) } ) = ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) )
41	38 39 40	3eqtr3rd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) = ( 𝑁 ‘ { 𝑌 , 𝑤 } ) )
42	10	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) = ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) )
43		prcom	⊢ { 𝑌 , 𝑤 } = { 𝑤 , 𝑌 }
44	43	fveq2i	⊢ ( 𝑁 ‘ { 𝑌 , 𝑤 } ) = ( 𝑁 ‘ { 𝑤 , 𝑌 } )
45	44	a1i	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑤 } ) = ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
46	41 42 45	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ) = ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
47	34 46	eqtrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 , ( 𝑤 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑤 , 𝑌 } ) )
48	31 47	neleqtrrd	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 , ( 𝑤 + 𝑌 ) } ) )
49	1 3 4 5 8 18 19 29 48	lspindp1	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { ( 𝑤 + 𝑌 ) } ) ∧ ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑤 + 𝑌 ) } ) ) )
50	49	simprd	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , ( 𝑤 + 𝑌 ) } ) )