HomeTheorem List (p. 352 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. 352 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 | sspadd1 35101 | A projective subspace sum is a superset of its first summand. (ssun1 3776 analog.) (Contributed by NM, 3-Jan-2012.) |
               ![/\](wedge.gif "/\"){kind=small}   
| ||
| Theorem | sspadd2 35102 | A projective subspace sum is a superset of its second summand. (ssun2 3777 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddss1 35103 | Subset law for projective subspace sum. (unss1 3782 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddss2 35104 | Subset law for projective subspace sum. (unss2 3784 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | paddss12 35105 | Subset law for projective subspace sum. (unss12 3785 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddasslem1 35106 | Lemma for paddass 35124. (Contributed by NM, 8-Jan-2012.) |
  
  
 | ||
| Theorem | paddasslem2 35107 | Lemma for paddass 35124. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem3 35108* | Lemma for paddass 35124. Restate projective space axiom ps-2 34764. (Contributed by NM, 8-Jan-2012.) |
 
| ||
| Theorem | paddasslem4 35109* | Lemma for paddass 35124. Combine paddasslem1 35106, paddasslem2 35107, and paddasslem3 35108. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem5 35110 |
Lemma for paddass 35124. Show by
contradiction. (Contributed
by NM, 8-Jan-2012.)
|
|
| ||
| Theorem | paddasslem6 35111 | Lemma for paddass 35124. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem7 35112 | Lemma for paddass 35124. Combine paddasslem5 35110 and paddasslem6 35111. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem8 35113 | Lemma for paddass 35124. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem9 35114 | Lemma for paddass 35124. Combine paddasslem7 35112 and paddasslem8 35113. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem10 35115 |
Lemma for paddass 35124. Use paddasslem4 35109 to eliminate from
paddasslem9 35114. (Contributed by NM, 9-Jan-2012.)
|
|
| ||
| Theorem | paddasslem11 35116 |
Lemma for paddass 35124. The case when .
(Contributed by NM,
11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem12 35117 |
Lemma for paddass 35124. The case when .
(Contributed by NM,
11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem13 35118 |
Lemma for paddass 35124. The case when . (Unlike
the proof in Maeda and Maeda, we don't need .)
(Contributed
by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem14 35119 |
Lemma for paddass 35124. Remove , , and
from antecedent of paddasslem10 35115, using
paddasslem11 35116, paddasslem12 35117, and paddasslem13 35118. (Contributed by
NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem15 35120 |
Lemma for paddass 35124. Use elpaddn0 35086 to eliminate and from
paddasslem14 35119. (Contributed by NM, 11-Jan-2012.)
|
| ||
| Theorem | paddasslem16 35121 |
Lemma for paddass 35124. Use elpaddn0 35086 to eliminate and from
paddasslem15 35120. (Contributed by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem17 35122 | Lemma for paddass 35124. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.) |
|
| ||
| Theorem | paddasslem18 35123 | Lemma for paddass 35124. Combine paddasslem16 35121 and paddasslem17 35122. (Contributed by NM, 12-Jan-2012.) |
|
| ||
| Theorem | paddass 35124 | 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 35125 | Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | padd4N 35126 | Rearrangement of 4 terms in a projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | paddidm 35127 | Projective subspace sum is idempotent. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 13-Jan-2012.) |
 
| ||
| Theorem | paddclN 35128 | 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 35129 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
|
| ||
| Theorem | paddssw2 35130 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
|
| ||
| Theorem | paddss 35131 | Subset law for projective subspace sum. (unss 3787 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | pmodlem1 35132* | Lemma for pmod1i 35134. (Contributed by NM, 9-Mar-2012.) |
 | ||
| Theorem | pmodlem2 35133 | Lemma for pmod1i 35134. (Contributed by NM, 9-Mar-2012.) |
|
| ||
| Theorem | pmod1i 35134 | The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012.) |
|
| ||
| Theorem | pmod2iN 35135 | Dual of the modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmodN 35136 | The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmodl42N 35137 | Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmapjoin 35138 | 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 35139 | The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012.) |
 | ||
| Theorem | pmapjat2 35140 | The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012.) |
| | ||
| Theorem | pmapjlln1 35141 |
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 35142 | A version of the modular law pmod1i 35134 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.) |
![./\](_.wedge.gif "./\"){kind=small}
 
| ||
| Theorem | atmod1i1 35143 | Version of modular law pmod1i 35134 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 35144 | Version of modular law pmod1i 35134 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 35145 | Version of modular law pmod1i 35134 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 35146 |
Version of modular law pmod1i 35134 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 35147 | Version of modular law pmod2iN 35135 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 35148 | Version of modular law pmod2iN 35135 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 35149 |
Version of modular law pmod1i 35134 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 35150 | 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 35151 | 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 35152 | 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 35153 | 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 35154 | Lemma for llnexchb2 35155. (Contributed by NM, 17-Nov-2012.) |
  | ||
| Theorem | llnexchb2 35155 | Line exchange property (compare cvlatexchb2 34622 for atoms). (Contributed by NM, 17-Nov-2012.) |
|
| ||
| Theorem | llnexch2N 35156 | Line exchange property (compare cvlatexch2 34624 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | dalawlem1 35157 |
Lemma for dalaw 35172. Special case of dath2 35023, where  is replaced
by
 . The remaining lemmas will
eliminate the conditions on the atoms imposed by dath2 35023.
(Contributed by NM, 6-Oct-2012.)
|
  
| ||
| Theorem | dalawlem2 35158 |
Lemma for dalaw 35172. Utility lemma that breaks
into a join of two pieces.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem3 35159 | Lemma for dalaw 35172. First piece of dalawlem5 35161. (Contributed by NM, 4-Oct-2012.) |
|
| ||
| Theorem | dalawlem4 35160 | Lemma for dalaw 35172. Second piece of dalawlem5 35161. (Contributed by NM, 4-Oct-2012.) |
|
| ||
| Theorem | dalawlem5 35161 |
Lemma for dalaw 35172. Special case to eliminate the requirement
in dalawlem1 35157.
(Contributed by NM, 4-Oct-2012.)
|
|
| ||
| Theorem | dalawlem6 35162 | Lemma for dalaw 35172. First piece of dalawlem8 35164. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem7 35163 | Lemma for dalaw 35172. Second piece of dalawlem8 35164. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem8 35164 |
Lemma for dalaw 35172. Special case to eliminate the requirement
in dalawlem1 35157.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem9 35165 |
Lemma for dalaw 35172. Special case to eliminate the requirement
in dalawlem1 35157.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem10 35166 | Lemma for dalaw 35172. Combine dalawlem5 35161, dalawlem8 35164, and dalawlem9 . (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem11 35167 | Lemma for dalaw 35172. First part of dalawlem13 35169. (Contributed by NM, 17-Sep-2012.) |
|
| ||
| Theorem | dalawlem12 35168 | Lemma for dalaw 35172. Second part of dalawlem13 35169. (Contributed by NM, 17-Sep-2012.) |
|
| ||
| Theorem | dalawlem13 35169 |
Lemma for dalaw 35172. Special case to eliminate the requirement
in dalawlem1 35157. (Contributed by NM,
6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem14 35170 | Lemma for dalaw 35172. Combine dalawlem10 35166 and dalawlem13 35169. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem15 35171 |
Lemma for dalaw 35172. Swap variable triples
and in
dalawlem14 35170, to obtain the elimination of the remaining
conditions in
dalawlem1 35157. (Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalaw 35172 |
Desargues' law, derived from Desargues' theorem dath 35022
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 35173 | Extend class notation with projective subspace closure. |
  | ||
| Definition | df-pclN 35174* |
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 35221.)
(Contributed by NM, 7-Sep-2013.)
|
  
   
 | ||
| Theorem | pclfvalN 35175* | The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
 | ||
| Theorem | pclvalN 35176* | Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclclN 35177 | Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | elpclN 35178* | Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
| ||
| Theorem | elpcliN 35179 | Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclssN 35180 | Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclssidN 35181 | A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
| | ||
| Theorem | pclidN 35182 | The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | pclbtwnN 35183 | 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 35184 | 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 35185 | 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 35186* | 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 35236. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
  | ||
| Theorem | pclcmpatN 35187* | 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 35188 | Extend class notation with polarity of projective subspace $m$. |
 | ||
| Definition | df-polarityN 35189* |
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.)
|
  | ||
| Theorem | polfvalN 35190* | The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
| ||
| Theorem | polvalN 35191* | Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | polval2N 35192 | Alternate expression for value of the projective subspace polarity function. Equation for polarity in [Holland95] p. 223. (Contributed by NM, 22-Jan-2012.) (New usage is discouraged.) |
| ||
| Theorem | polsubN 35193 | The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | polssatN 35194 | The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
| | ||
| Theorem | pol0N 35195 | The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | pol1N 35196 | The polarity of the whole projective subspace is the empty space. Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2pol0N 35197 | The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | polpmapN 35198 | The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2polpmapN 35199 | Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
| | ||
| Theorem | 2polvalN 35200 | Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |