Theorem lsppratlem5

Description: Lemma for lspprat . Combine the two cases and show a contradiction to U C. ( N{ X , Y } ) under the assumptions on x and y . (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	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
	lsppratlem1.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsppratlem1.x2	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
	lsppratlem1.y2	⊢ ( 𝜑 → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
Assertion	lsppratlem5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )

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		lsppratlem1.o	⊢ 0 = ( 0g ‘ 𝑊 )
10		lsppratlem1.x2	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
11		lsppratlem1.y2	⊢ ( 𝜑 → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑊 ∈ LVec )
13	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑈 ∈ 𝑆 )
14	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑋 ∈ 𝑉 )
15	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑌 ∈ 𝑉 )
16	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
17	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
18	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) )
20	1 2 3 12 13 14 15 16 9 17 18 19	lsppratlem3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )
21	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑊 ∈ LVec )
22	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑈 ∈ 𝑆 )
23	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑋 ∈ 𝑉 )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑌 ∈ 𝑉 )
25	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
26	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
27	11	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) )
29	1 2 3 21 22 23 24 25 9 26 27 28	lsppratlem4	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )
30	1 2 3 4 5 6 7 8 9 10 11	lsppratlem1	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ { 𝑌 } ) ∨ 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑌 } ) ) )
31	20 29 30	mpjaodan	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) )
32	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑊 ∈ LVec )
33	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑈 ∈ 𝑆 )
34	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑋 ∈ 𝑉 )
35	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑌 ∈ 𝑉 )
36	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑈 ⊊ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
37	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑥 ∈ ( 𝑈 ∖ { 0 } ) )
38	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑦 ∈ ( 𝑈 ∖ ( 𝑁 ‘ { 𝑥 } ) ) )
39		simprl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
40		simprr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) )
41	1 2 3 32 33 34 35 36 9 37 38 39 40	lsppratlem2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑥 , 𝑦 } ) ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )
42	31 41	mpdan	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑈 )