Theorem lspindpi

Description: Partial independence property. (Contributed by NM, 23-Apr-2015)

	Ref	Expression
Hypotheses	lspindpi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspindpi.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspindpi.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspindpi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspindpi.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspindpi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
	lspindpi.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
Assertion	lspindpi	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lspindpi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspindpi.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lspindpi.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
4		lspindpi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5		lspindpi.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
6		lspindpi.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
7		lspindpi.e	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
8		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9	3 8	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
10		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
11	10	lsssssubg	⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
12	9 11	syl	⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
13	1 10 2	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
14	9 5 13	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
15	12 14	sseldd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
16	1 10 2	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
17	9 6 16	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
18	12 17	sseldd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) )
19		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
20	19	lsmub1	⊢ ( ( ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
21	15 18 20	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
22	1 2 19 9 5 6	lsmpr	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
23	21 22	sseqtrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
24		sseq1	⊢ ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
25	23 24	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
26	1 10 2 9 5 6	lspprcl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
27	1 10 2 9 26 4	ellspsn5b	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
28	25 27	sylibrd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
29	28	necon3bd	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
30	7 29	mpd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
31	19	lsmub2	⊢ ( ( ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑍 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
32	15 18 31	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑍 } ) ) )
33	32 22	sseqtrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
34		sseq1	⊢ ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑍 } ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑍 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
35	33 34	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑍 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
36	35 27	sylibrd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑍 } ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
37	36	necon3bd	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ) )
38	7 37	mpd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
39	30 38	jca	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ) )