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 = ( 0_g ‘ 𝑊 )
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 = ( 0_g ‘ 𝑊 )
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 } ) → 𝑈 = ( 𝑁 ‘ { 𝑥 } ) ) )

Metamath Proof Explorer

Theorem lsppratlem6

Proof