Metamath Proof Explorer

Theorem lsppratlem6

Description: Lemma for lspprat . Negating the assumption on y , we arrive close to the desired conclusion. (Contributed by NM, 29-Aug-2014)

Ref Expression
Hypotheses lspprat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspprat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspprat.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspprat.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspprat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lspprat.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspprat.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspprat.p ⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
lsppratlem6.o ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion lsppratlem6 ( 𝜑 → ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) → 𝑈 = ( 𝑁 ‘ { 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 lspprat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspprat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspprat.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspprat.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lspprat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 lspprat.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 lspprat.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 lspprat.p ⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
9 lsppratlem6.o ⊢ 0 = ( 0g ‘ 𝑊 )
10 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
11 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑊 ∈ LVec )
12 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑈 ∈ 𝑆 )
13 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑋 ∈ 𝑉 )
14 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑌 ∈ 𝑉 )
15 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
18 1 2 3 11 12 13 14 15 9 16 17 lsppratlem5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )
19 ssnpss ⊢ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 → ¬ 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
20 18 19 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) ) ) → ¬ 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
21 20 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → ( 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) → ¬ 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
22 10 21 mt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → ¬ 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
23 22 eq0rdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) = ∅ )
24 ssdif0 ⊢ ( 𝑈 ⊆ ( 𝑁 ‘ { 𝑥 } ) ↔ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) = ∅ )
25 23 24 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → 𝑈 ⊆ ( 𝑁 ‘ { 𝑥 } ) )
26 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
27 4 26 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → 𝑊 ∈ LMod )
29 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → 𝑈 ∈ 𝑆 )
30 eldifi ⊢ ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) → 𝑥 ∈ 𝑈 )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → 𝑥 ∈ 𝑈 )
32 2 3 28 29 31 ellspsn5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ 𝑈 )
33 25 32 eqssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑈 ∖ { 0 } ) ) → 𝑈 = ( 𝑁 ‘ { 𝑥 } ) )
34 33 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑈 ∖ { 0 } ) → 𝑈 = ( 𝑁 ‘ { 𝑥 } ) ) )