HomeTheorem List (p. 370 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 370 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lcd0v2 36901 | The zero functional in the set of functionals with closed kernels. (Contributed by NM, 27-Mar-2015.) |
             LDual    LCDual      ![/\](wedge.gif "/\"){kind=small}  | ||
| Theorem | lcd0vvalN 36902 | Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
   Scalar LCDual  | ||
| Theorem | lcd0vcl 36903 | Closure of the zero functional in the set of functionals with closed kernels. (Contributed by NM, 15-Mar-2015.) |
| LCDual
| ||
| Theorem | lcd0vs 36904 | A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015.) |
 Scalar LCDual 
 | ||
| Theorem | lcdvs0N 36905 | A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
| Scalar LCDual
| ||
| Theorem | lcdvsub 36906 | The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015.) |
Scalar     
LCDual 
  
 | ||
| Theorem | lcdvsubval 36907 | The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015.) |
| Scalar LCDual
| ||
| Theorem | lcdlss 36908* | Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
 LCDual  LFnl  LKer LDual         | ||
| Theorem | lcdlss2N 36909 | Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
| LCDual LDual | ||
| Theorem | lcdlsp 36910 | Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015.) |
LDual   LCDual  | ||
| Theorem | lcdlkreqN 36911 | Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
LKer LCDual   | ||
| Theorem | lcdlkreq2N 36912 | Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
Scalar LKer LCDual
 ![\](setminus.gif "\"){kind=small}
| ||
| Syntax | cmpd 36913 | Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels. |
 mapd | ||
| Definition | df-mapd 36914* | Extend class notation with a one-to-one onto (mapd1o 36937), order-preserving (mapdord 36927) map, called a projectivity (definition of projectivity in [Baer] p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015.) |
mapd      LFnl LKer LKer
LKer | ||
| Theorem | mapdffval 36915* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
|
mapd LFnl LKer LKer LKer | ||
| Theorem | mapdfval 36916* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
| LFnl LKer mapd | ||
| Theorem | mapdval 36917* | Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.) |
| LFnl LKer mapd
| ||
| Theorem | mapdvalc 36918* | Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.) |
LFnl LKer mapd  | ||
| Theorem | mapdval2N 36919* | Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
LFnl LKer mapd   | ||
| Theorem | mapdval3N 36920* | Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
LFnl LKer mapd  | ||
| Theorem | mapdval4N 36921* |
Value of projectivity from vector space H to dual space. TODO: 1. This
is shorter than others - make it the official def? (but is not as
obvious that it is ) 2. The
unneeded direction of lcfl8a 36792 has
awkward -
add another thm with only one direction of it? 3. Swap
and
? (Contributed by NM, 31-Jan-2015.)
(New usage is discouraged.)
|
| LFnl LKer mapd | ||
| Theorem | mapdval5N 36922* | Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
| LFnl LKer mapd | ||
| Theorem | mapdordlem1a 36923* | Lemma for mapdord 36927. (Contributed by NM, 27-Jan-2015.) |
 LSHyp LFnl LKer 
 | ||
| Theorem | mapdordlem1bN 36924* | Lemma for mapdord 36927. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
| | ||
| Theorem | mapdordlem1 36925* | Lemma for mapdord 36927. (Contributed by NM, 27-Jan-2015.) |
| | ||
| Theorem | mapdordlem2 36926* |
Lemma for mapdord 36927. Ordering property of projectivity .
TODO: This was proved using some hacked-up older proofs. Maybe
simplify; get rid of the hypothesis. (Contributed by NM,
27-Jan-2015.)
|
| mapd LSAtoms LFnl LSHyp LKer
| ||
| Theorem | mapdord 36927 | Ordering property of the map defined by df-mapd 36914. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.) |
| mapd
| ||
| Theorem | mapd11 36928 | The map defined by df-mapd 36914 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.) |
| mapd
| ||
| Theorem | mapddlssN 36929 | The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 36945 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
| mapd LDual | ||
| Theorem | mapdsn 36930* | Value of the map defined by df-mapd 36914 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
| mapd LFnl LKer
| ||
| Theorem | mapdsn2 36931* | Value of the map defined by df-mapd 36914 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
| mapd LFnl LKer
| ||
| Theorem | mapdsn3 36932 | Value of the map defined by df-mapd 36914 at the span of a singleton. (Contributed by NM, 17-Feb-2015.) |
mapd LFnl LKer LDual  | ||
| Theorem | mapd1dim2lem1N 36933* | Value of the map defined by df-mapd 36914 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.) |
LSAtoms LFnl LKer mapd  | ||
| Theorem | mapdrvallem2 36934* | Lemma for mapdrval 36936. TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.) |
mapd LFnl LKer LDual  LSAtoms | ||
| Theorem | mapdrvallem3 36935* | Lemma for mapdrval 36936. (Contributed by NM, 2-Feb-2015.) |
| mapd LFnl LKer LDual LSAtoms | ||
| Theorem | mapdrval 36936* |
Given a dual subspace
(of functionals with closed kernels),
reconstruct the subspace that maps to it. (Contributed by NM,
12-Mar-2015.)
|
| mapd LFnl LKer LDual | ||
| Theorem | mapd1o 36937* |
The map defined by df-mapd 36914 is one-to-one and onto the set of dual
subspaces of functionals with closed kernels. This shows
satisfies part of the definition of projectivity of [Baer] p. 40. TODO:
change theorems leading to this (lcfr 36874, mapdrval 36936, lclkrs 36828,
lclkr 36822,...) to use ? TODO: maybe get rid of
$d's for
vs. ,. propagate to mapdrn 36938 and any others.
(Contributed by NM, 12-Mar-2015.)
|
mapd LFnl LKer LDual   | ||
| Theorem | mapdrn 36938* | Range of the map defined by df-mapd 36914. (Contributed by NM, 12-Mar-2015.) |
mapd LFnl LKer LDual  | ||
| Theorem | mapdunirnN 36939* | Union of the range of the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
mapd LFnl LKer  | ||
| Theorem | mapdrn2 36940 |
Range of the map defined by df-mapd 36914. TODO: this seems to be needed a
lot in hdmaprnlem3eN 37150 etc. Would it be better to change df-mapd 36914
theorems to use instead of ? (Contributed by
NM, 13-Mar-2015.)
|
| mapd LCDual | ||
| Theorem | mapdcnvcl 36941 | Closure of the converse of the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) |
mapd
 | ||
| Theorem | mapdcl 36942 | Closure the value of the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) |
| mapd
| ||
| Theorem | mapdcnvid1N 36943 | Converse of the value of the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
| mapd | ||
| Theorem | mapdsord 36944 | Strong ordering property of themap defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) |
mapd 
| ||
| Theorem | mapdcl2 36945 | The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.) |
| mapd LCDual | ||
| Theorem | mapdcnvid2 36946 | Value of the converse of the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) |
| mapd
| ||
| Theorem | mapdcnvordN 36947 | Ordering property of the converse of the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
| mapd
| ||
| Theorem | mapdcnv11N 36948 | The converse of the map defined by df-mapd 36914 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
| mapd
| ||
| Theorem | mapdcv 36949 | Covering property of the converse of the map defined by df-mapd 36914. (Contributed by NM, 14-Mar-2015.) |
mapd
 L LCDual 
L | ||
| Theorem | mapdincl 36950 | Closure of dual subspace intersection for the map defined by df-mapd 36914. (Contributed by NM, 12-Apr-2015.) |
| mapd LCDual
| ||
| Theorem | mapdin 36951 | Subspace intersection is preserved by the map defined by df-mapd 36914. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.) |
| mapd | ||
| Theorem | mapdlsmcl 36952 | Closure of dual subspace sum for the map defined by df-mapd 36914. (Contributed by NM, 13-Mar-2015.) |
mapd LCDual  
| ||
| Theorem | mapdlsm 36953 | Subspace sum is preserved by the map defined by df-mapd 36914. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.) |
mapd LCDual  | ||
| Theorem | mapd0 36954 | Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.) |
| mapd LCDual
| ||
| Theorem | mapdcnvatN 36955 | Atoms are preserved by the map defined by df-mapd 36914. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
| mapd LSAtoms LCDual LSAtoms | ||
| Theorem | mapdat 36956 | Atoms are preserved by the map defined by df-mapd 36914. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.) |
| mapd LSAtoms LCDual LSAtoms | ||
| Theorem | mapdspex 36957* | The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.) |
| mapd LCDual | ||
| Theorem | mapdn0 36958 | Transfer nonzero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.) |
mapd LCDual  | ||
| Theorem | mapdncol 36959 | Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
| mapd LCDual
| ||
| Theorem | mapdindp 36960 | Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
mapd LCDual 
| ||
| Theorem | mapdpglem1 36961 | Lemma for mapdpg 36995. Baer p. 44, last line: "(F(x-y))* =< (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.) |
| mapd
LCDual
| ||
| Theorem | mapdpglem2 36962* |
Lemma for mapdpg 36995. Baer p. 45, lines 1 and 2: "we have
(F(x-y))* =
Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d
locally to avoid clashes with later substitutions into .)
(Contributed by NM, 15-Mar-2015.)
|
| mapd
LCDual
| ||
| Theorem | mapdpglem2a 36963* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
| ||
| Theorem | mapdpglem3 36964* |
Lemma for mapdpg 36995. Baer p. 45, line 3: "infer...the
existence of a
number g in G and of an element z in (Fy)* such that t = gx'-z."
(We
scope $d  locally to avoid clashes with later
substitutions into .) (Contributed by NM, 18-Mar-2015.)
|
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem4N 36965* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem5N 36966* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem6 36967* | Lemma for mapdpg 36995. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem8 36968* | Lemma for mapdpg 36995. Baer p. 45, line 4: "...so that (F(x-y))* =< (Fy)*. This would imply that F(x-y) =< F(y)..." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem9 36969* | Lemma for mapdpg 36995. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem10 36970* | Lemma for mapdpg 36995. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem11 36971* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem12 36972* | Lemma for mapdpg 36995. TODO: Can some commonality with mapdpglem6 36967 through mapdpglem11 36971 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem13 36973* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem14 36974* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem15 36975* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem16 36976* | Lemma for mapdpg 36995. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem17N 36977* | Lemma for mapdpg 36995. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
mapd
LCDual
Scalar
 | ||
| Theorem | mapdpglem18 36978* | Lemma for mapdpg 36995. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem19 36979* | Lemma for mapdpg 36995. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem20 36980* | Lemma for mapdpg 36995. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem21 36981* | Lemma for mapdpg 36995. (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem22 36982* | Lemma for mapdpg 36995. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.) |
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem23 36983* |
Lemma for mapdpg 36995. Baer p. 45, line 10: "and so y'
meets all our
requirements." Our is Baer's y'. (Contributed by NM,
20-Mar-2015.)
|
| mapd
LCDual
Scalar
| ||
| Theorem | mapdpglem30a 36984 | Lemma for mapdpg 36995. (Contributed by NM, 22-Mar-2015.) |
| mapd LCDual
| ||
| Theorem | mapdpglem30b 36985 | Lemma for mapdpg 36995. (Contributed by NM, 22-Mar-2015.) |
mapd LCDual
| ||
| Theorem | mapdpglem25 36986 | Lemma for mapdpg 36995. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.) |
| mapd LCDual
| ||
| Theorem | mapdpglem26 36987* |
Lemma for mapdpg 36995. Baer p. 45 line 14: "Consequently
there exist
numbers u,v in G neither of which is 0 such that y = uy''
and..."
(We scope $d 
locally to avoid clashes with later
substitutions into .) (Contributed by NM, 22-Mar-2015.)
|
| mapd LCDual
Scalar
| ||
| Theorem | mapdpglem27 36988* | Lemma for mapdpg 36995. Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015.) |
| mapd LCDual
Scalar
| ||
| Theorem | mapdpglem29 36989* | Lemma for mapdpg 36995. Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (Contributed by NM, 22-Mar-2015.) |
| mapd LCDual
Scalar
| ||
| Theorem | mapdpglem28 36990* | Lemma for mapdpg 36995. Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015.) |
| mapd LCDual
Scalar
| ||
| Theorem | mapdpglem30 36991* |
Lemma for mapdpg 36995. Baer p. 45 line 18: "Hence we deduce
(from
mapdpglem28 36990, using lvecindp2 19139) that v = 1 and v = u...". TODO:
would it be shorter to have only the part
and use
mapdpglem28.u2 in mapdpglem31 36992? (Contributed by NM,
22-Mar-2015.)
|
| mapd LCDual
Scalar
| ||
| Theorem | mapdpglem31 36992* | Lemma for mapdpg 36995. Baer p. 45 line 19: "...and we have consequently that y' = y'', as we claimed." (Contributed by NM, 23-Mar-2015.) |
| mapd LCDual
Scalar
| ||
| Theorem | mapdpglem24 36993* | Lemma for mapdpg 36995. Existence part - consolidate hypotheses in mapdpglem23 36983. (Contributed by NM, 21-Mar-2015.) |
| mapd LCDual
| ||
| Theorem | mapdpglem32 36994* | Lemma for mapdpg 36995. Uniqueness part - consolidate hypotheses in mapdpglem31 36992. (Contributed by NM, 23-Mar-2015.) |
| mapd LCDual
| ||
| Theorem | mapdpg 36995* |
Part 1 of proof of the first fundamental theorem of projective geometry.
Part (1) in [Baer] p. 44. Our notation
corresponds to Baer's as
follows: for
*, for F(), for G(),
for x, for x',
for y, for y'. TODO: Rename
variables
per mapdhval 37013. (Contributed by NM, 22-Mar-2015.)
|
mapd LCDual
| ||
| Theorem | baerlem3lem1 36996 | Lemma for baerlem3 37002. (Contributed by NM, 9-Apr-2015.) |
Scalar      
| ||
| Theorem | baerlem5alem1 36997 | Lemma for baerlem5a 37003. (Contributed by NM, 13-Apr-2015.) |
|
Scalar
| ||
| Theorem | baerlem5blem1 36998 | Lemma for baerlem5b 37004. (Contributed by NM, 9-Apr-2015.) |
|
Scalar
| ||
| Theorem | baerlem3lem2 36999 | Lemma for baerlem3 37002. (Contributed by NM, 9-Apr-2015.) |
|
Scalar
| ||
| Theorem | baerlem5alem2 37000 | Lemma for baerlem5a 37003. (Contributed by NM, 9-Apr-2015.) |
|
Scalar | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |