Step | Hyp | Ref
| Expression |
1 | | mapdpg.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | mapdpg.m |
. . 3
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) |
3 | | mapdpg.u |
. . 3
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
4 | | mapdpg.v |
. . 3
⊢ 𝑉 = (Base‘𝑈) |
5 | | mapdpg.s |
. . 3
⊢ − =
(-g‘𝑈) |
6 | | mapdpg.n |
. . 3
⊢ 𝑁 = (LSpan‘𝑈) |
7 | | mapdpg.c |
. . 3
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
8 | | mapdpg.k |
. . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
9 | | mapdpg.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
10 | 9 | eldifad 3903 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
11 | | mapdpg.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
12 | 11 | eldifad 3903 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
13 | | eqid 2739 |
. . 3
⊢
(LSSum‘𝐶) =
(LSSum‘𝐶) |
14 | | mapdpg.j |
. . 3
⊢ 𝐽 = (LSpan‘𝐶) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 10, 12, 13, 14 | mapdpglem2 39666 |
. 2
⊢ (𝜑 → ∃𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌})))(𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) |
16 | 8 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
17 | 10 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → 𝑋 ∈ 𝑉) |
18 | 12 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → 𝑌 ∈ 𝑉) |
19 | | mapdpg.f |
. . . . 5
⊢ 𝐹 = (Base‘𝐶) |
20 | | simp2 1135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌})))) |
21 | | eqid 2739 |
. . . . 5
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
22 | | eqid 2739 |
. . . . 5
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
23 | | eqid 2739 |
. . . . 5
⊢ (
·𝑠 ‘𝐶) = ( ·𝑠
‘𝐶) |
24 | | mapdpg.r |
. . . . 5
⊢ 𝑅 = (-g‘𝐶) |
25 | | mapdpg.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
26 | 25 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → 𝐺 ∈ 𝐹) |
27 | | mapdpg.e |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) |
28 | 27 | 3ad2ant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) |
29 | 1, 2, 3, 4, 5, 6, 7, 16, 17, 18, 13, 14, 19, 20, 21, 22, 23, 24, 26, 28 | mapdpglem3 39668 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → ∃𝑔 ∈ (Base‘(Scalar‘𝑈))∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) |
30 | 16 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
31 | 17 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑋 ∈ 𝑉) |
32 | 18 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑌 ∈ 𝑉) |
33 | | simp12 1202 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌})))) |
34 | 26 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝐺 ∈ 𝐹) |
35 | 28 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐺})) |
36 | | mapdpg.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑈) |
37 | | mapdpg.ne |
. . . . . . . . 9
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
38 | 37 | 3ad2ant1 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
39 | 38 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
40 | | simp13 1203 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) |
41 | | eqid 2739 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑈)) =
(0g‘(Scalar‘𝑈)) |
42 | | simp2l 1197 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑔 ∈ (Base‘(Scalar‘𝑈))) |
43 | | simp2r 1198 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) |
44 | | simp3 1136 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) |
45 | | eldifsni 4728 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) → 𝑋 ≠ 0 ) |
46 | 9, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ 0 ) |
47 | 46 | 3ad2ant1 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → 𝑋 ≠ 0 ) |
48 | 47 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑋 ≠ 0 ) |
49 | | eldifsni 4728 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (𝑉 ∖ { 0 }) → 𝑌 ≠ 0 ) |
50 | 11, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ≠ 0 ) |
51 | 50 | 3ad2ant1 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → 𝑌 ≠ 0 ) |
52 | 51 | 3ad2ant1 1131 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → 𝑌 ≠ 0 ) |
53 | | eqid 2739 |
. . . . . . 7
⊢
(((invr‘(Scalar‘𝑈))‘𝑔)( ·𝑠
‘𝐶)𝑧) =
(((invr‘(Scalar‘𝑈))‘𝑔)( ·𝑠
‘𝐶)𝑧) |
54 | 1, 2, 3, 4, 5, 6, 7, 30, 31, 32, 13, 14, 19, 33, 21, 22, 23, 24, 34, 35, 36, 39, 40, 41, 42, 43, 44, 48, 52, 53 | mapdpglem23 39687 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) ∧ (𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) ∧ 𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧)) → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) |
55 | 54 | 3exp 1117 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → ((𝑔 ∈ (Base‘(Scalar‘𝑈)) ∧ 𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))) → (𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧) → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))))) |
56 | 55 | rexlimdvv 3223 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → (∃𝑔 ∈ (Base‘(Scalar‘𝑈))∃𝑧 ∈ (𝑀‘(𝑁‘{𝑌}))𝑡 = ((𝑔( ·𝑠
‘𝐶)𝐺)𝑅𝑧) → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))) |
57 | 29, 56 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌}))) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡})) → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) |
58 | 57 | rexlimdv3a 3216 |
. 2
⊢ (𝜑 → (∃𝑡 ∈ ((𝑀‘(𝑁‘{𝑋}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑌})))(𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{𝑡}) → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)})))) |
59 | 15, 58 | mpd 15 |
1
⊢ (𝜑 → ∃ℎ ∈ 𝐹 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐺𝑅ℎ)}))) |