Theorem dvh4dimN

Description: There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvh3dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvh3dim.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvh3dim.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dvh3dim.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dvh3dim.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dvh3dim.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	dvh3dim.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	dvh3dim2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion	dvh4dimN	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )

Proof

Step	Hyp	Ref	Expression
1		dvh3dim.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvh3dim.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dvh3dim.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		dvh3dim.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5		dvh3dim.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		dvh3dim.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7		dvh3dim.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8		dvh3dim2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9	1 2 3 4 5 7 8	dvh3dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
11		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12	1 2 5	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
13		prssi	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → { 𝑌 , 𝑍 } ⊆ 𝑉 )
14	7 8 13	syl2anc	⊢ ( 𝜑 → { 𝑌 , 𝑍 } ⊆ 𝑉 )
15	3 11 4 12 14	lspun0	⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
16		tprot	⊢ { ( 0g ‘ 𝑈 ) , 𝑌 , 𝑍 } = { 𝑌 , 𝑍 , ( 0g ‘ 𝑈 ) }
17		df-tp	⊢ { 𝑌 , 𝑍 , ( 0g ‘ 𝑈 ) } = ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } )
18	16 17	eqtr2i	⊢ ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) , 𝑌 , 𝑍 }
19		tpeq1	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 , 𝑍 } = { ( 0g ‘ 𝑈 ) , 𝑌 , 𝑍 } )
20	18 19	eqtr4id	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , 𝑌 , 𝑍 } )
21	20	fveq2d	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ ( { 𝑌 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
22	15 21	sylan9req	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
23	22	eleq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
24	23	notbid	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
25	24	rexbidv	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
26	10 25	mpbid	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
27	1 2 3 4 5 6 8	dvh3dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
29		prssi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → { 𝑋 , 𝑍 } ⊆ 𝑉 )
30	6 8 29	syl2anc	⊢ ( 𝜑 → { 𝑋 , 𝑍 } ⊆ 𝑉 )
31	3 11 4 12 30	lspun0	⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
32		df-tp	⊢ { 𝑋 , 𝑍 , ( 0g ‘ 𝑈 ) } = ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } )
33		tpcomb	⊢ { 𝑋 , 𝑍 , ( 0g ‘ 𝑈 ) } = { 𝑋 , ( 0g ‘ 𝑈 ) , 𝑍 }
34	32 33	eqtr3i	⊢ ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , ( 0g ‘ 𝑈 ) , 𝑍 }
35		tpeq2	⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 , 𝑍 } = { 𝑋 , ( 0g ‘ 𝑈 ) , 𝑍 } )
36	34 35	eqtr4id	⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , 𝑌 , 𝑍 } )
37	36	fveq2d	⊢ ( 𝑌 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ ( { 𝑋 , 𝑍 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
38	31 37	sylan9req	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑍 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
39	38	eleq2d	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
40	39	notbid	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
41	40	rexbidv	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
42	28 41	mpbid	⊢ ( ( 𝜑 ∧ 𝑌 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
43	1 2 3 4 5 6 7	dvh3dim	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
45		prssi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
46	6 7 45	syl2anc	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
47	3 11 4 12 46	lspun0	⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
48		tpeq3	⊢ ( 𝑍 = ( 0g ‘ 𝑈 ) → { 𝑋 , 𝑌 , 𝑍 } = { 𝑋 , 𝑌 , ( 0g ‘ 𝑈 ) } )
49		df-tp	⊢ { 𝑋 , 𝑌 , ( 0g ‘ 𝑈 ) } = ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } )
50	48 49	eqtr2di	⊢ ( 𝑍 = ( 0g ‘ 𝑈 ) → ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } ) = { 𝑋 , 𝑌 , 𝑍 } )
51	50	fveq2d	⊢ ( 𝑍 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
52	47 51	sylan9req	⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
53	52	eleq2d	⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
54	53	notbid	⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
55	54	rexbidv	⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
56	44 55	mpbid	⊢ ( ( 𝜑 ∧ 𝑍 = ( 0g ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
57	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
58	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ∈ 𝑉 )
59	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ∈ 𝑉 )
60	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑍 ∈ 𝑉 )
61		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
62		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑌 ≠ ( 0g ‘ 𝑈 ) )
63		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → 𝑍 ≠ ( 0g ‘ 𝑈 ) )
64	1 2 3 4 57 58 59 60 11 61 62 63	dvh4dimlem	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑌 ≠ ( 0g ‘ 𝑈 ) ∧ 𝑍 ≠ ( 0g ‘ 𝑈 ) ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
65	26 42 56 64	pm2.61da3ne	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )