HomeTheorem List (p. 347 of 370)
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. 347 of 370) | < 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-25539) |
Hilbert Space Explorer
(25540-27064) |
Users' Mathboxes
(27065-36941) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 2llnma1 34601 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012.) |
         
 ![./\](_.wedge.gif "./\"){kind=small}
      ![/\](wedge.gif "/\"){kind=small}   
 
| ||
| Theorem | 2llnma3r 34602 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013.) |
 | ||
| Theorem | 2llnma2 34603 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012.) |
|
| ||
| Theorem | 2llnma2rN 34604 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlema1N 34605 | A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 29-Apr-2012.) (New usage is discouraged.) |
 
     
| ||
| Theorem | cdlema2N 34606 | A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 9-May-2012.) (New usage is discouraged.) |
 
| ||
| Theorem | cdlemblem 34607 | Lemma for cdlemb 34608. (Contributed by NM, 8-May-2012.) |
  
   
| ||
| Theorem | cdlemb 34608* | Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 8-May-2012.) |
 | ||
| Syntax | cpadd 34609 | Extend class notation with projective subspace sum. |
   | ||
| Definition | df-padd 34610* | Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.) |
           
 | ||
| Theorem | paddfval 34611* | Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.) |
| ||
| Theorem | paddval 34612* | Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.) |
| ||
| Theorem | elpadd 34613* | Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.) |
  
| ||
| Theorem | elpaddn0 34614* | Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.) |
 | ||
| Theorem | paddvaln0N 34615* | Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpaddri 34616 | Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | elpaddatriN 34617 | Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpaddat 34618* | Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpaddatiN 34619* | Consequence of membership in a projective subspace sum with a point. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpadd2at 34620 | Membership in a projective subspace sum of two points. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpadd2at2 34621 | Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012.) |
|
| ||
| Theorem | paddunssN 34622 | Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpadd0 34623 | Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011.) |
|
| ||
| Theorem | paddval0 34624 | Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | padd01 34625 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
| | ||
| Theorem | padd02 34626 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | paddcom 34627 | Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddssat 34628 | A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | sspadd1 34629 | A projective subspace sum is a superset of its first summand. (ssun1 3667 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | sspadd2 34630 | A projective subspace sum is a superset of its second summand. (ssun2 3668 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddss1 34631 | Subset law for projective subspace sum. (unss1 3673 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddss2 34632 | Subset law for projective subspace sum. (unss2 3675 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | paddss12 34633 | Subset law for projective subspace sum. (unss12 3676 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddasslem1 34634 | Lemma for paddass 34652. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem2 34635 | Lemma for paddass 34652. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem3 34636* | Lemma for paddass 34652. Restate projective space axiom ps-2 34292. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem4 34637* | Lemma for paddass 34652. Combine paddasslem1 34634, paddasslem2 34635, and paddasslem3 34636. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem5 34638 |
Lemma for paddass 34652. Show by
contradiction. (Contributed
by NM, 8-Jan-2012.)
|
|
| ||
| Theorem | paddasslem6 34639 | Lemma for paddass 34652. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem7 34640 | Lemma for paddass 34652. Combine paddasslem5 34638 and paddasslem6 34639. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem8 34641 | Lemma for paddass 34652. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem9 34642 | Lemma for paddass 34652. Combine paddasslem7 34640 and paddasslem8 34641. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem10 34643 |
Lemma for paddass 34652. Use paddasslem4 34637 to eliminate from
paddasslem9 34642. (Contributed by NM, 9-Jan-2012.)
|
|
| ||
| Theorem | paddasslem11 34644 |
Lemma for paddass 34652. The case when .
(Contributed by NM,
11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem12 34645 |
Lemma for paddass 34652. The case when .
(Contributed by NM,
11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem13 34646 |
Lemma for paddass 34652. The case when . (Unlike
the proof in Maeda and Maeda, we don't need .)
(Contributed
by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem14 34647 |
Lemma for paddass 34652. Remove , , and
from antecedent of paddasslem10 34643, using
paddasslem11 34644, paddasslem12 34645, and paddasslem13 34646. (Contributed by
NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem15 34648 |
Lemma for paddass 34652. Use elpaddn0 34614 to eliminate and from
paddasslem14 34647. (Contributed by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem16 34649 |
Lemma for paddass 34652. Use elpaddn0 34614 to eliminate and from
paddasslem15 34648. (Contributed by NM, 11-Jan-2012.)
|
|
| ||
| Theorem | paddasslem17 34650 | Lemma for paddass 34652. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.) |
|
| ||
| Theorem | paddasslem18 34651 | Lemma for paddass 34652. Combine paddasslem16 34649 and paddasslem17 34650. (Contributed by NM, 12-Jan-2012.) |
|
| ||
| Theorem | paddass 34652 | 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 34653 | Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | padd4N 34654 | Rearrangement of 4 terms in a projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | paddidm 34655 | Projective subspace sum is idempotent. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 13-Jan-2012.) |
| ||
| Theorem | paddclN 34656 | 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 34657 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
|
| ||
| Theorem | paddssw2 34658 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
|
| ||
| Theorem | paddss 34659 | Subset law for projective subspace sum. (unss 3678 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | pmodlem1 34660* | Lemma for pmod1i 34662. (Contributed by NM, 9-Mar-2012.) |
 | ||
| Theorem | pmodlem2 34661 | Lemma for pmod1i 34662. (Contributed by NM, 9-Mar-2012.) |
|
| ||
| Theorem | pmod1i 34662 | The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012.) |
|
| ||
| Theorem | pmod2iN 34663 | Dual of the modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmodN 34664 | The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmodl42N 34665 | Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | pmapjoin 34666 | 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 34667 | The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012.) |
| | ||
| Theorem | pmapjat2 34668 | The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012.) |
| | ||
| Theorem | pmapjlln1 34669 |
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 34670 | A version of the modular law pmod1i 34662 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.) |
|
| ||
| Theorem | atmod1i1 34671 | Version of modular law pmod1i 34662 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 34672 | Version of modular law pmod1i 34662 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 34673 | Version of modular law pmod1i 34662 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 34674 |
Version of modular law pmod1i 34662 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 34675 | Version of modular law pmod2iN 34663 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 34676 | Version of modular law pmod2iN 34663 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 34677 |
Version of modular law pmod1i 34662 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 34678 | 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 34679 | 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 34680 | 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 34681 | 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 34682 | Lemma for llnexchb2 34683. (Contributed by NM, 17-Nov-2012.) |
 | ||
| Theorem | llnexchb2 34683 | Line exchange property (compare cvlatexchb2 34150 for atoms). (Contributed by NM, 17-Nov-2012.) |
|
| ||
| Theorem | llnexch2N 34684 | Line exchange property (compare cvlatexch2 34152 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | dalawlem1 34685 |
Lemma for dalaw 34700. Special case of dath2 34551, where is replaced
by
 . The remaining lemmas will
eliminate the conditions on the atoms imposed by dath2 34551.
(Contributed by NM, 6-Oct-2012.)
|
  
| ||
| Theorem | dalawlem2 34686 |
Lemma for dalaw 34700. Utility lemma that breaks
into a join of two pieces.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem3 34687 | Lemma for dalaw 34700. First piece of dalawlem5 34689. (Contributed by NM, 4-Oct-2012.) |
|
| ||
| Theorem | dalawlem4 34688 | Lemma for dalaw 34700. Second piece of dalawlem5 34689. (Contributed by NM, 4-Oct-2012.) |
|
| ||
| Theorem | dalawlem5 34689 |
Lemma for dalaw 34700. Special case to eliminate the requirement
in dalawlem1 34685.
(Contributed by NM, 4-Oct-2012.)
|
|
| ||
| Theorem | dalawlem6 34690 | Lemma for dalaw 34700. First piece of dalawlem8 34692. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem7 34691 | Lemma for dalaw 34700. Second piece of dalawlem8 34692. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem8 34692 |
Lemma for dalaw 34700. Special case to eliminate the requirement
in dalawlem1 34685.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem9 34693 |
Lemma for dalaw 34700. Special case to eliminate the requirement
in dalawlem1 34685.
(Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem10 34694 | Lemma for dalaw 34700. Combine dalawlem5 34689, dalawlem8 34692, and dalawlem9 . (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem11 34695 | Lemma for dalaw 34700. First part of dalawlem13 34697. (Contributed by NM, 17-Sep-2012.) |
|
| ||
| Theorem | dalawlem12 34696 | Lemma for dalaw 34700. Second part of dalawlem13 34697. (Contributed by NM, 17-Sep-2012.) |
|
| ||
| Theorem | dalawlem13 34697 |
Lemma for dalaw 34700. Special case to eliminate the requirement
in dalawlem1 34685. (Contributed by NM,
6-Oct-2012.)
|
|
| ||
| Theorem | dalawlem14 34698 | Lemma for dalaw 34700. Combine dalawlem10 34694 and dalawlem13 34697. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | dalawlem15 34699 |
Lemma for dalaw 34700. Swap variable triples
and in
dalawlem14 34698, to obtain the elimination of the remaining
conditions in
dalawlem1 34685. (Contributed by NM, 6-Oct-2012.)
|
|
| ||
| Theorem | dalaw 34700 |
Desargues' law, derived from Desargues' theorem dath 34550
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.)
|
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |