Home Metamath Proof ExplorerTheorem List (p. 315 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)

Theorem List for Metamath Proof Explorer - 31401-31500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcdlemk40f 31401* TODO: fix comment. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk41 31402* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.)

Theoremcdlemkfid1N 31403 Lemma for cdlemkfid3N 31407. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkid1 31404 Lemma for cdlemkid 31418. (Contributed by NM, 24-Jul-2013.)

Theoremcdlemkfid2N 31405 Lemma for cdlemkfid3N 31407. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkid2 31406* Lemma for cdlemkid 31418. (Contributed by NM, 24-Jul-2013.)

Theoremcdlemkfid3N 31407* TODO: is this useful or should it be deleted? (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

Theoremcdlemky 31408* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up stuff. represents in cdlemk31 31378. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemkyu 31409* Convert between function and explicit forms. represents in cdlemkuu 31377. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemkyuu 31410* cdlemkyu 31409 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemk11ta 31411* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemk19ylem 31412* Lemma for cdlemk19y 31414. (Contributed by NM, 30-Jul-2013.)

Theoremcdlemk11tb 31413* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. cdlemk11ta 31411 with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013.)

Theoremcdlemk19y 31414* cdlemk19 31351 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.)

Theoremcdlemkid3N 31415* Lemma for cdlemkid 31418. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkid4 31416* Lemma for cdlemkid 31418. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemkid5 31417* Lemma for cdlemkid 31418. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemkid 31418* The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemk35s 31419* Substitution version of cdlemk35 31394. (Contributed by NM, 22-Jul-2013.)

Theoremcdlemk35s-id 31420* Substitution version of cdlemk35 31394. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk39s 31421* Substitution version of cdlemk39 31398. TODO: Can any commonality with cdlemk35s 31419 be exploited? (Contributed by NM, 23-Jul-2013.)

Theoremcdlemk39s-id 31422* Substitution version of cdlemk39 31398 with non-identity requirement on removed. TODO: Can any commonality with cdlemk35s 31419 be exploited? (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk42 31423* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.)

Theoremcdlemk19xlem 31424* Lemma for cdlemk19x 31425. (Contributed by NM, 30-Jul-2013.)

Theoremcdlemk19x 31425* cdlemk19 31351 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.)

Theoremcdlemk42yN 31426* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk11tc 31427* Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemk11t 31428* Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119. , stand for g, h. represents tau. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemk45 31429* Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119. , stand for g, h. represents tau. They do not explicitly mention the requirement . (Contributed by NM, 22-Jul-2013.)

Theoremcdlemk46 31430* Part of proof of Lemma K of [Crawley] p. 118. Line 38 (last line), p. 119. , stand for g, h. represents tau. (Contributed by NM, 22-Jul-2013.)

Theoremcdlemk47 31431* Part of proof of Lemma K of [Crawley] p. 118. Line 2, p. 120. , stand for g, h. represents tau. (Contributed by NM, 22-Jul-2013.)

Theoremcdlemk48 31432* Part of proof of Lemma K of [Crawley] p. 118. Line 4, p. 120. , stand for g, h. represents tau. (Contributed by NM, 22-Jul-2013.)

Theoremcdlemk49 31433* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 120. , stand for g, h. represents tau. (Contributed by NM, 23-Jul-2013.)

Theoremcdlemk50 31434* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 31436? (Contributed by NM, 23-Jul-2013.)

Theoremcdlemk51 31435* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 31436? (Contributed by NM, 23-Jul-2013.)

Theoremcdlemk52 31436* Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. (Contributed by NM, 23-Jul-2013.)

Theoremcdlemk53a 31437* Lemma for cdlemk53 31439. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk53b 31438* Lemma for cdlemk53 31439. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk53 31439* Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120. , stand for g, h. represents tau. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk54 31440* Part of proof of Lemma K of [Crawley] p. 118. Line 10, p. 120. , stand for g, h. represents tau. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk55a 31441* Lemma for cdlemk55 31443. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk55b 31442* Lemma for cdlemk55 31443. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk55 31443* Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. , stand for g, h. represents tau. (Contributed by NM, 26-Jul-2013.)

TheoremcdlemkyyN 31444* Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up stuff. (Contributed by NM, 21-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk43N 31445* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 31-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk35u 31446* Substitution version of cdlemk35 31394. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk55u1 31447* Lemma for cdlemk55u 31448. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk55u 31448* Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. , stand for g, h. represents tau. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk39u1 31449* Lemma for cdlemk39u 31450. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk39u 31450* Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by . (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk19u1 31451* cdlemk19 31351 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk19u 31452* Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with , , . (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk56 31453* Part of Lemma K of [Crawley] p. 118. Line 11, p. 120, "tau is in Delta" i.e. is a trace-preserving endormorphism. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk19w 31454* Use a fixed element to eliminate in cdlemk19u 31452. (Contributed by NM, 1-Aug-2013.)

Theoremcdlemk56w 31455* Use a fixed element to eliminate in cdlemk56 31453. (Contributed by NM, 1-Aug-2013.)

Theoremcdlemk 31456* Lemma K of [Crawley] p.