dalemrot - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalemrot		Structured version Unicode version

Theorem dalemrot 32931

Description: Lemma for dath 33010. Rotate triangles

and

to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalemc.l
dalemc.j	$.\/$
dalemc.a
dalemrot.y	$.\/$ $.\/$
dalemrot.z	$.\/$ $.\/$

**Assertion**
Ref	Expression
dalemrot	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

**Proof of Theorem dalemrot**
Step	Hyp	Ref	Expression
1		dalema.ph	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2	1	dalemkehl 32897	. . . 4
3		dalemc.a	. . . . 5
4	1, 3	dalemceb 32912	. . . 4
5	2, 4	jca 534	. . 3 $/\$
6	1	dalemqea 32901	. . . 4
7	1	dalemrea 32902	. . . 4
8	1	dalempea 32900	. . . 4
9	6, 7, 8	3jca 1185	. . 3 $/\$ $/\$
10	1	dalemtea 32904	. . . 4
11	1	dalemuea 32905	. . . 4
12	1	dalemsea 32903	. . . 4
13	10, 11, 12	3jca 1185	. . 3 $/\$ $/\$
14	5, 9, 13	3jca 1185	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		dalemc.j	. . . . 5 $.\/$
16	1, 15, 3	dalemqrprot 32922	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
17		dalemrot.y	. . . . 5 $.\/$ $.\/$
18	1	dalemyeo 32906	. . . . 5
19	17, 18	syl5eqelr 2513	. . . 4 $.\/$ $.\/$
20	16, 19	eqeltrd 2508	. . 3 $.\/$ $.\/$
21	15, 3	hlatjrot 32647	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	2, 10, 11, 12, 21	syl13anc 1266	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
23		dalemrot.z	. . . . 5 $.\/$ $.\/$
24	1	dalemzeo 32907	. . . . 5
25	23, 24	syl5eqelr 2513	. . . 4 $.\/$ $.\/$
26	22, 25	eqeltrd 2508	. . 3 $.\/$ $.\/$
27	20, 26	jca 534	. 2 $.\/$ $.\/$ $/\$ $.\/$ $.\/$
28		simp312 1153	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
29	1, 28	sylbi 198	. . . 4 $.\/$
30		simp313 1154	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	1, 30	sylbi 198	. . . 4 $.\/$
32	1	dalem-clpjq 32911	. . . 4 $.\/$
33	29, 31, 32	3jca 1185	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
34		simp322 1156	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	1, 34	sylbi 198	. . . 4 $.\/$
36		simp323 1157	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	1, 36	sylbi 198	. . . 4 $.\/$
38		simp321 1155	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39	1, 38	sylbi 198	. . . 4 $.\/$
40	35, 37, 39	3jca 1185	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
41	1	dalemclqjt 32909	. . . 4 $.\/$
42	1	dalemclrju 32910	. . . 4 $.\/$
43	1	dalemclpjs 32908	. . . 4 $.\/$
44	41, 42, 43	3jca 1185	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	33, 40, 44	3jca 1185	. 2 $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46	14, 27, 45	3jca 1185	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867 class class class wbr 4417

cfv 5592 (class class class)co 6296

cbs 15073

cple 15149

cjn 16133

catm 32538

chlt 32625

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-ral 2778 df-rex 2779 df-reu 2780 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-op 4000 df-uni 4214 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-id 4760 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-preset 16117 df-poset 16135 df-lub 16164 df-glb 16165 df-join 16166 df-meet 16167 df-lat 16236 df-ats 32542 df-atl 32573 df-cvlat 32597 df-hlat 32626

This theorem is referenced by: dalemeea 32937 dalem6 32942 dalem7 32943 dalem11 32948 dalem12 32949 dalem29 32975 dalem30 32976 dalem31N 32977 dalem32 32978 dalem33 32979 dalem34 32980 dalem35 32981 dalem36 32982 dalem37 32983 dalem40 32986 dalem46 32992 dalem47 32993 dalem49 32995 dalem50 32996 dalem58 33004 dalem59 33005

W3C validator