HomeTheorem List (p. 323 of 325)
Unicode version.
| Home |
Metamath
Proof Explorer Theorem List (p. 323 of 325) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | baerlem5abmN 32201 |
An equality that holds when  ,  ,  are independent
(non-colinear) vectors. Subtraction versions of first and second
equations of part (5) in [Baer] p. 46,
conjoined to share commonality in
their proofs. TODO: Delete if not be needed. (Contributed by NM,
24-May-2015.) (New usage is discouraged.)
|
                    
     ![\](setminus.gif "\"){kind=small}     ![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | mapdindp0 32202 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
| ||
| Theorem | mapdindp1 32203 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
|
| ||
| Theorem | mapdindp2 32204 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
|
| ||
| Theorem | mapdindp3 32205 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
|
| ||
| Theorem | mapdindp4 32206 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
|
| ||
| Theorem | mapdhval 32207* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
            
     
| ||
| Theorem | mapdhval0 32208* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
 | ||
| Theorem | mapdhval2 32209* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
|
| ||
| Theorem | mapdhcl 32210* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
  mapd  LCDual 
| ||
| Theorem | mapdheq 32211* | Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.) |
mapd LCDual
 | ||
| Theorem | mapdheq2 32212* | Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.) |
|
mapd LCDual
| ||
| Theorem | mapdheq2biN 32213* | Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 32212 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdheq4lem 32214* | Lemma for mapdheq4 32215. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.) |
|
mapd LCDual
| ||
| Theorem | mapdheq4 32215* | Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.) |
|
mapd LCDual
| ||
| Theorem | mapdh6lem1N 32216* | Lemma for mapdh6N 32230. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.) |
mapd LCDual
| ||
| Theorem | mapdh6lem2N 32217* | Lemma for mapdh6N 32230. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6aN 32218* | Lemma for mapdh6N 32230. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6b0N 32219* | Lemmma for mapdh6N 32230. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6bN 32220* | Lemmma for mapdh6N 32230. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6cN 32221* | Lemmma for mapdh6N 32230. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6dN 32222* | Lemmma for mapdh6N 32230. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6eN 32223* | Lemmma for mapdh6N 32230. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6fN 32224* | Lemmma for mapdh6N 32230. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6gN 32225* | Lemmma for mapdh6N 32230. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6hN 32226* | Lemmma for mapdh6N 32230. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6iN 32227* |
Lemmma for mapdh6N 32230. Eliminate auxiliary vector .
(Contributed by NM, 1-May-2015.) (New usage is discouraged.)
|
|
mapd LCDual
| ||
| Theorem | mapdh6jN 32228* |
Lemmma for mapdh6N 32230. Eliminate { Y } ) = ( N
hypothesis. (Contributed by NM, 1-May-2015.)
(New usage is discouraged.)
|
|
mapd LCDual
| ||
| Theorem | mapdh6kN 32229* | Lemmma for mapdh6N 32230. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
|
mapd LCDual
| ||
| Theorem | mapdh6N 32230* |
Part (6) of [Baer] p. 47 line 6. Note that we
use
which is equivalent to Baer's "Fx
(Fy + Fz)" by lspdisjb 16153. TODO: If $ds with and becomes
a problem later, cbv's on variables here to get rid of them. .
Maybe reorder hypotheses in lemmas to the more consistent order of this
theorem, so they can be shared with this theorem. (Contributed by NM,
1-May-2015.) (New usage is discouraged.)
|
| LCDual mapd
| ||
| Theorem | mapdh7eN 32231* | Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). (Note: 1 of 6 and 2 of 6 are hypotheses a and b.) (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
LCDual mapd
| ||
| Theorem | mapdh7cN 32232* | Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
| LCDual mapd
| ||
| Theorem | mapdh7dN 32233* | Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
| LCDual mapd
| ||
| Theorem | mapdh7fN 32234* | Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
| LCDual mapd
| ||
| Theorem | mapdh75e 32235* |
Part (7) of [Baer] p. 48 line 10 (5 of 6 cases).
, ,
are Baer's u, v, w. (Note: Cases 1 of 6 and 2 of 6 are hypotheses
mapdh75b here and mapdh75a in mapdh75cN 32236.) (Contributed by NM,
2-May-2015.)
|
| LCDual mapd
| ||
| Theorem | mapdh75cN 32236* | Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
| LCDual mapd
| ||
| Theorem | mapdh75d 32237* | Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.) |
| LCDual mapd
| ||
| Theorem | mapdh75fN 32238* | Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
| LCDual mapd
| ||
| Syntax | chvm 32239 | Extend class notation with vector to dual map. |
HVMap | ||
| Definition | df-hvmap 32240* |
Extend class notation with a map from each nonzero vector to a
unique nonzero functional in the closed kernel dual space. (We could
extend it to include the zero vector, but that is unnecessary for our
purposes.) TODO: This pattern is used several times earlier e.g.
lcf1o 32034, dochfl1 31959- should we update those to use this
definition?
(Contributed by NM, 23-Mar-2015.)
|
HVMap 
 Scalar    | ||
| Theorem | hvmapffval 32241* | Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) |
|
HVMap
Scalar | ||
| Theorem | hvmapfval 32242* | Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) |
   Scalar HVMap
| ||
| Theorem | hvmapval 32243* | Value of map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) |
| Scalar HVMap
| ||
| Theorem | hvmapvalvalN 32244* | Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.) |
| Scalar HVMap
| ||
| Theorem | hvmapidN 32245 | The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.) |
Scalar 
 HVMap
| ||
| Theorem | hvmap1o 32246* |
The vector to functional map provides a bijection from nonzero vectors
to nonzero
functionals with closed kernels . (Contributed
by NM, 27-Mar-2015.)
|
LFnl  LKer LDual
  HVMap
  | ||
| Theorem | hvmapclN 32247* | Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) (New usage is discouraged.) |
| LFnl LKer LDual
HVMap
| ||
| Theorem | hvmap1o2 32248 |
The vector to functional map provides a bijection from nonzero vectors
to nonzero
functionals with closed kernels . (Contributed
by NM, 27-Mar-2015.)
|
| LCDual
HVMap
| ||
| Theorem | hvmapcl2 32249 | Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) |
| LCDual
HVMap
| ||
| Theorem | hvmaplfl 32250 | The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015.) |
| LFnl HVMap
| ||
| Theorem | hvmaplkr 32251 | Kernel of the vector to functional map. TODO: make this become lcfrlem11 32036. (Contributed by NM, 29-Mar-2015.) |
| LKer HVMap
| ||
| Theorem | mapdhvmap 32252 | Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 32189. Equation 10 of [Baer] p. 48. (Contributed by NM, 29-Mar-2015.) |
LCDual mapd  HVMap
| ||
| Theorem | lspindp5 32253 |
Obtain an independent vector set from a vector
dependent on
and and another
independent set
.
(Here we don't show the
part of the
independence, which
passes straight through. We also don't show nonzero vector requirements
that are redundant for this theorem. Different orderings can be
obtained using lspexch 16156 and prcom 3842.) (Contributed by NM,
4-May-2015.)
|
|
| ||
| Theorem | hdmaplem1 32254 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) |
| ||
| Theorem | hdmaplem2N 32255 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
|
| ||
| Theorem | hdmaplem3 32256 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) |
|
| ||
| Theorem | hdmaplem4 32257 | Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) |
|
| ||
| Theorem | mapdh8a 32258* | Part of Part (8) in [Baer] p. 48. (Contributed by NM, 5-May-2015.) |
LCDual mapd
 | ||