| Step | Hyp | Ref
| Expression |
| 1 | | mapdh8a.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
| 2 | | mapdh8a.u |
. . . . . . 7
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 3 | | mapdh8a.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
| 4 | | mapdh8a.s |
. . . . . . 7
⊢ − =
(-g‘𝑈) |
| 5 | | mapdh8a.o |
. . . . . . 7
⊢ 0 =
(0g‘𝑈) |
| 6 | | mapdh8a.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑈) |
| 7 | | mapdh8a.c |
. . . . . . 7
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
| 8 | | mapdh8a.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐶) |
| 9 | | mapdh8a.r |
. . . . . . 7
⊢ 𝑅 = (-g‘𝐶) |
| 10 | | mapdh8a.q |
. . . . . . 7
⊢ 𝑄 = (0g‘𝐶) |
| 11 | | mapdh8a.j |
. . . . . . 7
⊢ 𝐽 = (LSpan‘𝐶) |
| 12 | | mapdh8a.m |
. . . . . . 7
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
| 13 | | mapdh8a.i |
. . . . . . 7
⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
| 14 | | mapdh8a.k |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 16 | | mapdh8h.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
| 17 | 16 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → 𝐹 ∈ 𝐷) |
| 18 | | mapdh8h.mn |
. . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) |
| 19 | 18 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) |
| 20 | | mapdh9a.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
| 21 | 20 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → 𝑋 ∈ (𝑉 ∖ { 0 })) |
| 22 | | simp3ll 1245 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → 𝑧 ∈ (𝑉 ∖ { 0 })) |
| 23 | | simp3rl 1247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → 𝑤 ∈ (𝑉 ∖ { 0 })) |
| 24 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋})) |
| 25 | 24 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋})) |
| 26 | 25 | necomd 2996 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑧})) |
| 27 | | simprrl 781 |
. . . . . . . . 9
⊢ (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋})) |
| 28 | 27 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋})) |
| 29 | 28 | necomd 2996 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑤})) |
| 30 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})) |
| 31 | 30 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})) |
| 32 | | simprrr 782 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})) |
| 33 | 32 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})) |
| 34 | | mapdh9a.t |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
| 35 | 34 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → 𝑇 ∈ 𝑉) |
| 36 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 15, 17, 19, 21, 22, 23, 26, 29, 31, 33, 35 | mapdh8 41790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) ∧ ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) = (𝐼‘〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉)) |
| 37 | 36 | 3exp 1120 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉) → (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) = (𝐼‘〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉)))) |
| 38 | 37 | ralrimivv 3200 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) = (𝐼‘〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉))) |
| 39 | 20 | eldifad 3963 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 40 | 1, 2, 3, 6, 14, 39, 34 | dvh3dim 41448 |
. . . . . . 7
⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) |
| 41 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 42 | 1, 2, 14 | dvhlmod 41112 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ LMod) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → 𝑈 ∈ LMod) |
| 44 | 3, 41, 6, 42, 39, 34 | lspprcl 20976 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘{𝑋, 𝑇}) ∈ (LSubSp‘𝑈)) |
| 45 | 44 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → (𝑁‘{𝑋, 𝑇}) ∈ (LSubSp‘𝑈)) |
| 46 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → 𝑧 ∈ 𝑉) |
| 47 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) |
| 48 | 5, 41, 43, 45, 46, 47 | lssneln0 20951 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → 𝑧 ∈ (𝑉 ∖ { 0 })) |
| 49 | 1, 2, 14 | dvhlvec 41111 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ LVec) |
| 50 | 49 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → 𝑈 ∈ LVec) |
| 51 | 39 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → 𝑋 ∈ 𝑉) |
| 52 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → 𝑇 ∈ 𝑉) |
| 53 | 3, 6, 50, 46, 51, 52, 47 | lspindpi 21134 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) |
| 54 | 48, 53 | jca 511 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇})) → (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) |
| 55 | 54 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))))) |
| 56 | 55 | reximdva 3168 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → ∃𝑧 ∈ 𝑉 (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))))) |
| 57 | 40, 56 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) |
| 58 | 14 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 59 | 16 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → 𝐹 ∈ 𝐷) |
| 60 | 18 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) |
| 61 | 20 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → 𝑋 ∈ (𝑉 ∖ { 0 })) |
| 62 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → 𝑧 ∈ 𝑉) |
| 63 | | simprrl 781 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋})) |
| 64 | 63 | necomd 2996 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑧})) |
| 65 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 58, 59, 60, 61, 62, 64 | mapdhcl 41729 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑋, 𝐹, 𝑧〉) ∈ 𝐷) |
| 66 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑋, 𝐹, 𝑧〉) = (𝐼‘〈𝑋, 𝐹, 𝑧〉)) |
| 67 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → 𝑧 ∈ (𝑉 ∖ { 0 })) |
| 68 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 58, 59, 60, 61, 67, 65, 64 | mapdheq 41730 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → ((𝐼‘〈𝑋, 𝐹, 𝑧〉) = (𝐼‘〈𝑋, 𝐹, 𝑧〉) ↔ ((𝑀‘(𝑁‘{𝑧})) = (𝐽‘{(𝐼‘〈𝑋, 𝐹, 𝑧〉)}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑧)})) = (𝐽‘{(𝐹𝑅(𝐼‘〈𝑋, 𝐹, 𝑧〉))})))) |
| 69 | 66, 68 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → ((𝑀‘(𝑁‘{𝑧})) = (𝐽‘{(𝐼‘〈𝑋, 𝐹, 𝑧〉)}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑧)})) = (𝐽‘{(𝐹𝑅(𝐼‘〈𝑋, 𝐹, 𝑧〉))}))) |
| 70 | 69 | simpld 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝑀‘(𝑁‘{𝑧})) = (𝐽‘{(𝐼‘〈𝑋, 𝐹, 𝑧〉)})) |
| 71 | 34 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → 𝑇 ∈ 𝑉) |
| 72 | | simprrr 782 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})) |
| 73 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 58, 65, 70, 67, 71, 72 | mapdhcl 41729 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) ∈ 𝐷) |
| 74 | 73 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) ∈ 𝐷)) |
| 75 | 74 | ancld 550 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) ∈ 𝐷))) |
| 76 | 75 | reximdva 3168 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ 𝑉 (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → ∃𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) ∈ 𝐷))) |
| 77 | 57, 76 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) ∈ 𝐷)) |
| 78 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (𝑧 ∈ (𝑉 ∖ { 0 }) ↔ 𝑤 ∈ (𝑉 ∖ { 0 }))) |
| 79 | | sneq 4636 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → {𝑧} = {𝑤}) |
| 80 | 79 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑁‘{𝑧}) = (𝑁‘{𝑤})) |
| 81 | 80 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ↔ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}))) |
| 82 | 80 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}) ↔ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))) |
| 83 | 81, 82 | anbi12d 632 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})) ↔ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) |
| 84 | 78, 83 | anbi12d 632 |
. . . . . 6
⊢ (𝑧 = 𝑤 → ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ↔ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))))) |
| 85 | | oteq1 4882 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → 〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉 = 〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) |
| 86 | | oteq3 4884 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → 〈𝑋, 𝐹, 𝑧〉 = 〈𝑋, 𝐹, 𝑤〉) |
| 87 | 86 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝐼‘〈𝑋, 𝐹, 𝑧〉) = (𝐼‘〈𝑋, 𝐹, 𝑤〉)) |
| 88 | 87 | oteq2d 4886 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → 〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉 = 〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉) |
| 89 | 85, 88 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → 〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉 = 〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉) |
| 90 | 89 | fveq2d 6910 |
. . . . . 6
⊢ (𝑧 = 𝑤 → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) = (𝐼‘〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉)) |
| 91 | 84, 90 | reusv3 5405 |
. . . . 5
⊢
(∃𝑧 ∈
𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) ∈ 𝐷) → (∀𝑧 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) = (𝐼‘〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉)) ↔ ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 92 | 77, 91 | syl 17 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝑉 ∀𝑤 ∈ 𝑉 (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) ∧ (𝑤 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇})))) → (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉) = (𝐼‘〈𝑤, (𝐼‘〈𝑋, 𝐹, 𝑤〉), 𝑇〉)) ↔ ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 93 | 38, 92 | mpbid 232 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) |
| 94 | | ioran 986 |
. . . . . . . 8
⊢ (¬
(𝑧 ∈ (𝑁‘{𝑋}) ∨ 𝑧 ∈ (𝑁‘{𝑇})) ↔ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) |
| 95 | | elun 4153 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) ↔ (𝑧 ∈ (𝑁‘{𝑋}) ∨ 𝑧 ∈ (𝑁‘{𝑇}))) |
| 96 | 94, 95 | xchnxbir 333 |
. . . . . . 7
⊢ (¬
𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) ↔ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) |
| 97 | 42 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) → 𝑈 ∈ LMod) |
| 98 | 3, 41, 6 | lspsncl 20975 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
| 99 | 42, 39, 98 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
| 100 | 99 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
| 101 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) → 𝑧 ∈ 𝑉) |
| 102 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) → ¬ 𝑧 ∈ (𝑁‘{𝑋})) |
| 103 | 5, 41, 97, 100, 101, 102 | lssneln0 20951 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇}))) → 𝑧 ∈ (𝑉 ∖ { 0 })) |
| 104 | 103 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → ((¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → 𝑧 ∈ (𝑉 ∖ { 0 }))) |
| 105 | 42 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋})) → 𝑈 ∈ LMod) |
| 106 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋})) → 𝑧 ∈ 𝑉) |
| 107 | 39 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋})) → 𝑋 ∈ 𝑉) |
| 108 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋})) → ¬ 𝑧 ∈ (𝑁‘{𝑋})) |
| 109 | 3, 6, 105, 106, 107, 108 | lspsnne2 21120 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑋})) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋})) |
| 110 | 109 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → (¬ 𝑧 ∈ (𝑁‘{𝑋}) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}))) |
| 111 | 42 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → 𝑈 ∈ LMod) |
| 112 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → 𝑧 ∈ 𝑉) |
| 113 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → 𝑇 ∈ 𝑉) |
| 114 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → ¬ 𝑧 ∈ (𝑁‘{𝑇})) |
| 115 | 3, 6, 111, 112, 113, 114 | lspsnne2 21120 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑉) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})) |
| 116 | 115 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → (¬ 𝑧 ∈ (𝑁‘{𝑇}) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) |
| 117 | 110, 116 | anim12d 609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → ((¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇})))) |
| 118 | 104, 117 | jcad 512 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → ((¬ 𝑧 ∈ (𝑁‘{𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑇})) → (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))))) |
| 119 | 96, 118 | biimtrid 242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → (𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))))) |
| 120 | 119 | imim1d 82 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉) → (((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)) → (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 121 | 120 | ralimdva 3167 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)) → ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 122 | 121 | reximdv 3170 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 ((𝑧 ∈ (𝑉 ∖ { 0 }) ∧ ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑇}))) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)) → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 123 | 93, 122 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) |
| 124 | 3, 6, 42, 39, 34 | lspprid1 20995 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑇})) |
| 125 | 41, 6, 42, 44, 124 | ellspsn5 20994 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑇})) |
| 126 | 3, 6, 42, 39, 34 | lspprid2 20996 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (𝑁‘{𝑋, 𝑇})) |
| 127 | 41, 6, 42, 44, 126 | ellspsn5 20994 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑇}) ⊆ (𝑁‘{𝑋, 𝑇})) |
| 128 | 125, 127 | unssd 4192 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) ⊆ (𝑁‘{𝑋, 𝑇})) |
| 129 | 128 | ssneld 3985 |
. . . . 5
⊢ (𝜑 → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → ¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})))) |
| 130 | 129 | reximdv 3170 |
. . . 4
⊢ (𝜑 → (∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑇}) → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})))) |
| 131 | 40, 130 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇}))) |
| 132 | | reusv1 5397 |
. . 3
⊢
(∃𝑧 ∈
𝑉 ¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → (∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)) ↔ ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 133 | 131, 132 | syl 17 |
. 2
⊢ (𝜑 → (∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)) ↔ ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉)))) |
| 134 | 123, 133 | mpbird 257 |
1
⊢ (𝜑 → ∃!𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝑋}) ∪ (𝑁‘{𝑇})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑋, 𝐹, 𝑧〉), 𝑇〉))) |