HomeTheorem List (p. 351 of 374)
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. 351 of 374) | < 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-25658) |
Hilbert Space Explorer
(25659-27183) |
Users' Mathboxes
(27184-37324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elpaddat 35001* | Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.) |
         
        
![/\](wedge.gif "/\"){kind=small}       
     | ||
| Theorem | elpaddatiN 35002* | Consequence of membership in a projective subspace sum with a point. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
 | ||
| Theorem | elpadd2at 35003 | Membership in a projective subspace sum of two points. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpadd2at2 35004 | Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012.) |
|
| ||
| Theorem | paddunssN 35005 | Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012.) (New usage is discouraged.) |
 
 | ||
| Theorem | elpadd0 35006 | Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011.) |
 | ||
| Theorem | paddval0 35007 | Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | padd01 35008 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
| | ||
| Theorem | padd02 35009 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | paddcom 35010 | Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddssat 35011 | A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | sspadd1 35012 | A projective subspace sum is a superset of its first summand. (ssun1 3672 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | sspadd2 35013 | A projective subspace sum is a superset of its second summand. (ssun2 3673 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddss1 35014 | Subset law for projective subspace sum. (unss1 3678 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddss2 35015 | Subset law for projective subspace sum. (unss2 3680 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | paddss12 35016 | Subset law for projective subspace sum. (unss12 3681 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddasslem1 35017 | Lemma for paddass 35035. (Contributed by NM, 8-Jan-2012.) |
 
| ||
| Theorem | paddasslem2 35018 | Lemma for paddass 35035. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem3 35019* | Lemma for paddass 35035. Restate projective space axiom ps-2 34675. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem4 35020* | Lemma for paddass 35035. Combine paddasslem1 35017, paddasslem2 35018, and paddasslem3 35019. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem5 35021 |
Lemma for paddass 35035. Show by
contradiction. (Contributed
by NM, 8-Jan-2012.)
|
|
| ||
| Theorem | paddasslem6 35022 | Lemma for paddass 35035. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem7 35023 | Lemma for paddass 35035. Combine paddasslem5 35021 and paddasslem6 35022. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem8 35024 | Lemma for paddass 35035. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem9 35025 | Lemma for paddass 35035. Combine paddasslem7 35023 and paddasslem8 35024. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem10 35026 |
Lemma for paddass 35035. Use paddasslem4 35020 to eliminate from
paddasslem9 35025. (Contributed by NM, 9-Jan-2012.)
|
|
| ||
| Theorem | paddasslem11 35027 |
Lemma for paddass 35035. The case when .
(Contributed by NM,
11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem12 35028 |
Lemma for paddass 35035. The case when .
(Contributed by NM,
11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem13 35029 |
Lemma for paddass 35035. The case when . (Unlike
the proof in Maeda and Maeda, we don't need .)
(Contributed
by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem14 35030 |
Lemma for paddass 35035. Remove , , and
from antecedent of paddasslem10 35026, using
paddasslem11 35027, paddasslem12 35028, and paddasslem13 35029. (Contributed by
NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem15 35031 |
Lemma for paddass 35035. Use elpaddn0 34997 to eliminate and from
paddasslem14 35030. (Contributed by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem16 35032 |
Lemma for paddass 35035. Use elpaddn0 34997 to eliminate and from
paddasslem15 35031. (Contributed by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem17 35033 | Lemma for paddass 35035. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.) |
|
| ||
| Theorem | paddasslem18 35034 | Lemma for paddass 35035. Combine paddasslem16 35032 and paddasslem17 35033. (Contributed by NM, 12-Jan-2012.) |
|
| ||
| Theorem | paddass 35035 | Projective subspace sum is associative. Equation 16.2.1 of [MaedaMaeda] p. 68. In our version, the subspaces do not have to be nonempty. (Contributed by NM, 29-Dec-2011.) |
|
| ||
| Theorem | padd12N 35036 | Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | padd4N 35037 | Rearrangement of 4 terms in a projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | paddidm 35038 | Projective subspace sum is idempotent. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 13-Jan-2012.) |
| ||
| Theorem | paddclN 35039 | The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | paddssw1 35040 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
|
| ||
| Theorem | paddssw2 35041 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
|
| ||
| Theorem | paddss 35042 | Subset law for projective subspace sum. (unss 3683 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | pmodlem1 35043* | Lemma for pmod1i 35045. (Contributed by NM, 9-Mar-2012.) |
 | ||
| Theorem | pmodlem2 35044 | Lemma for pmod1i 35045. (Contributed by NM, 9-Mar-2012.) |
|
| ||
| Theorem | pmod1i 35045 | The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012.) |
|
| ||
| Theorem | pmod2iN 35046 | Dual of the modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmodN 35047 | The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmodl42N 35048 | Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmapjoin 35049 | The projective map of the join of two lattice elements. Part of Equation 15.5.3 of [MaedaMaeda] p. 63. (Contributed by NM, 27-Jan-2012.) |
  
| ||
| Theorem | pmapjat1 35050 | The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012.) |
| | ||
| Theorem | pmapjat2 35051 | The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012.) |
| | ||
| Theorem | pmapjlln1 35052 |
The projective map of the join of a lattice element and a lattice line
(expressed as the join of two atoms).
(Contributed by NM,
16-Sep-2012.)
|
|
| ||
| Theorem | hlmod1i 35053 | A version of the modular law pmod1i 35045 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.) |
![./\](_.wedge.gif "./\"){kind=small}
 
| ||
| Theorem | atmod1i1 35054 | Version of modular law pmod1i 35045 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 11-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
| ||
| Theorem | atmod1i1m 35055 | Version of modular law pmod1i 35045 that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | atmod1i2 35056 | Version of modular law pmod1i 35045 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | llnmod1i2 35057 |
Version of modular law pmod1i 35045 that holds in a Hilbert lattice, when
one element is a lattice line (expressed as the join ).
(Contributed by NM, 16-Sep-2012.) (Revised by Mario Carneiro,
10-May-2013.)
|
|
| ||
| Theorem | atmod2i1 35058 | Version of modular law pmod2iN 35046 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | atmod2i2 35059 | Version of modular law pmod2iN 35046 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | llnmod2i2 35060 |
Version of modular law pmod1i 35045 that holds in a Hilbert lattice, when
one element is a lattice line (expressed as the join ).
(Contributed by NM, 16-Sep-2012.) (Revised by Mario Carneiro,
10-May-2013.)
|
|
| ||
| Theorem | atmod3i1 35061 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | atmod3i2 35062 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | atmod4i1 35063 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
|
| ||
| Theorem | atmod4i2 35064 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012.) (Revised by Mario Carneiro, 10-Mar-2013.) |
|
| ||
| Theorem | llnexchb2lem 35065 | Lemma for llnexchb2 35066. (Contributed by NM, 17-Nov-2012.) |
  | ||
| Theorem | llnexchb2 35066 | Line exchange property (compare cvlatexchb2 34533 for atoms). (Contributed by NM, 17-Nov-2012.) |
|
| ||
| Theorem | llnexch2N 35067 | Line exchange property (compare cvlatexch2 34535 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | dalawlem1 35068 |
Lemma for dalaw 35083. Special case of dath2 34934, where  is replaced
by
 . The remaining lemmas will
eliminate the conditions on the atoms imposed by dath2 34934.
(Contributed by NM, 6-Oct-2012.)
|
  
| ||
| Theorem | dalawlem2 35069 |
Lemma for dalaw 35083. Utility lemma that breaks
into a join of two pieces.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem3 35070 | Lemma for dalaw 35083. First piece of dalawlem5 35072. (Contributed by NM, 4-Oct-2012.) |
|
| ||
| Theorem | dalawlem4 35071 | Lemma for dalaw 35083. Second piece of dalawlem5 35072. (Contributed by NM, 4-Oct-2012.) |
|
| ||
| Theorem | dalawlem5 35072 |
Lemma for dalaw 35083. Special case to eliminate the requirement
in dalawlem1 35068.
(Contributed by NM, 4-Oct-2012.)
|
|
| ||
| Theorem | dalawlem6 35073 | Lemma for dalaw 35083. First piece of dalawlem8 35075. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem7 35074 | Lemma for dalaw 35083. Second piece of dalawlem8 35075. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem8 35075 |
Lemma for dalaw 35083. Special case to eliminate the requirement
in dalawlem1 35068.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem9 35076 |
Lemma for dalaw 35083. Special case to eliminate the requirement
in dalawlem1 35068.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem10 35077 | Lemma for dalaw 35083. Combine dalawlem5 35072, dalawlem8 35075, and dalawlem9 . (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem11 35078 | Lemma for dalaw 35083. First part of dalawlem13 35080. (Contributed by NM, 17-Sep-2012.) |
|
| ||
| Theorem | dalawlem12 35079 | Lemma for dalaw 35083. Second part of dalawlem13 35080. (Contributed by NM, 17-Sep-2012.) |
|
| ||
| Theorem | dalawlem13 35080 |
Lemma for dalaw 35083. Special case to eliminate the requirement
in dalawlem1 35068. (Contributed by NM,
6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem14 35081 | Lemma for dalaw 35083. Combine dalawlem10 35077 and dalawlem13 35080. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem15 35082 |
Lemma for dalaw 35083. Swap variable triples
and in
dalawlem14 35081, to obtain the elimination of the remaining
conditions in
dalawlem1 35068. (Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalaw 35083 |
Desargues' law, derived from Desargues' theorem dath 34933
and with no
conditions on the atoms. If triples  
 and
are centrally perspective, i.e.
, then they
are
axially perspective. Theorem 13.3 of [Crawley] p. 110. (Contributed by
NM, 7-Oct-2012.)
|
|
| ||
| Syntax | cpclN 35084 | Extend class notation with projective subspace closure. |
  | ||
| Definition | df-pclN 35085* |
Projective subspace closure, which is the smallest projective subspace
containing an arbitrary set of atoms. The subspace closure of the union
of a set of projective subspaces is their supremum in .
Related to an analogous definition of closure used in Lemma 3.1.4 of
[PtakPulmannova] p. 68. (Note
that this closure is not necessarily one
of the closed projective subspaces  of df-psubclN 35132.)
(Contributed by NM, 7-Sep-2013.)
|
  
  
| ||
| Theorem | pclfvalN 35086* | The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
 | ||
| Theorem | pclvalN 35087* | Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclclN 35088 | Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | elpclN 35089* | Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
| ||
| Theorem | elpcliN 35090 | Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclssN 35091 | Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclssidN 35092 | A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
| | ||
| Theorem | pclidN 35093 | The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclbtwnN 35094 | A projective subspace sandwiched between a set of atoms and the set's projective subspace closure equals the closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclunN 35095 | The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclun2N 35096 | The projective subspace closure of the union of two subspaces equals their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
| | ||
| Theorem | pclfinN 35097* | The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of [PtakPulmannova] p. 72. Compare the closed subspace version pclfinclN 35147. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
  | ||
| Theorem | pclcmpatN 35098* | The set of projective subspaces is compactly atomistic: if an atom is in the projective subspace closure of a set of atoms, it also belongs to the projective subspace closure of a finite subset of that set. Analogous to Lemma 3.3.10 of [PtakPulmannova] p. 74. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Syntax | cpolN 35099 | Extend class notation with polarity of projective subspace $m$. |
 | ||
| Definition | df-polarityN 35100* |
Define polarity of projective subspace, which is a kind of complement of
the subspace. Item 2 in [Holland95]
p. 222 bottom. For more
generality, we define it for all subsets of atoms, not just projective
subspaces. The intersection with 
ensures it is defined
when  . (Contributed by NM, 23-Oct-2011.)
|
  | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |