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