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 |
⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) |