This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) ) )