Metamath Proof Explorer

Theorem lspindp5

Description: Obtain an independent vector set U , X , Y from a vector U dependent on X and Z and another independent set Z , X , Y . (Here we don't show the ( N{ X } ) =/= ( N{ Y } ) part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch and prcom .) (Contributed by NM, 4-May-2015)

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

Proof

Step Hyp Ref Expression
1 lspindp5.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspindp5.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lspindp5.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
4 lspindp5.y ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5 lspindp5.x ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
6 lspindp5.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
7 lspindp5.e ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑈 } ) )
8 lspindp5.m ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
9 ssel ⊢ ( ( 𝑁 ‘ { 𝑋 , 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → ( 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑈 } ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
10 7 9 syl5com ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
11 8 10 mtod ⊢ ( 𝜑 → ¬ ( 𝑁 ‘ { 𝑋 , 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
12 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
13 3 12 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
14 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
15 4 5 14 syl2anc ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
16 snsspr1 ⊢ { 𝑋 } ⊆ { 𝑋 , 𝑌 }
17 16 a1i ⊢ ( 𝜑 → { 𝑋 } ⊆ { 𝑋 , 𝑌 } )
18 1 2 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ∧ { 𝑋 } ⊆ { 𝑋 , 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
19 13 15 17 18 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
20 19 biantrurd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) )
21 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
22 21 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
23 13 22 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
24 1 21 2 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
25 13 4 24 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
26 23 25 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
27 1 21 2 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑈 } ) ∈ ( LSubSp ‘ 𝑊 ) )
28 13 6 27 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑈 } ) ∈ ( LSubSp ‘ 𝑊 ) )
29 23 28 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑈 } ) ∈ ( SubGrp ‘ 𝑊 ) )
30 1 21 2 13 4 5 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
31 23 30 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
32 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
33 32 lsmlub ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑈 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑈 } ) ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
34 26 29 31 33 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ( 𝑁 ‘ { 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑈 } ) ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
35 20 34 bitrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑈 } ) ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
36 1 21 2 13 30 6 lspsnel5 ⊢ ( 𝜑 → ( 𝑈 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
37 1 2 32 13 4 6 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑈 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑈 } ) ) )
38 37 sseq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑈 } ) ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
39 35 36 38 3bitr4d ⊢ ( 𝜑 → ( 𝑈 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 , 𝑈 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
40 11 39 mtbird ⊢ ( 𝜑 → ¬ 𝑈 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )