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 33659

Description: Lemma for dath 33738. 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 33625	. . . 4
3		dalemc.a	. . . . 5
4	1, 3	dalemceb 33640	. . . 4
5	2, 4	jca 532	. . 3 $/\$
6	1	dalemqea 33629	. . . 4
7	1	dalemrea 33630	. . . 4
8	1	dalempea 33628	. . . 4
9	6, 7, 8	3jca 1168	. . 3 $/\$ $/\$
10	1	dalemtea 33632	. . . 4
11	1	dalemuea 33633	. . . 4
12	1	dalemsea 33631	. . . 4
13	10, 11, 12	3jca 1168	. . 3 $/\$ $/\$
14	5, 9, 13	3jca 1168	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		dalemc.j	. . . . 5 $.\/$
16	1, 15, 3	dalemqrprot 33650	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
17		dalemrot.y	. . . . 5 $.\/$ $.\/$
18	1	dalemyeo 33634	. . . . 5
19	17, 18	syl5eqelr 2547	. . . 4 $.\/$ $.\/$
20	16, 19	eqeltrd 2542	. . 3 $.\/$ $.\/$
21	15, 3	hlatjrot 33375	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	2, 10, 11, 12, 21	syl13anc 1221	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
23		dalemrot.z	. . . . 5 $.\/$ $.\/$
24	1	dalemzeo 33635	. . . . 5
25	23, 24	syl5eqelr 2547	. . . 4 $.\/$ $.\/$
26	22, 25	eqeltrd 2542	. . 3 $.\/$ $.\/$
27	20, 26	jca 532	. 2 $.\/$ $.\/$ $/\$ $.\/$ $.\/$
28		simp312 1136	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
29	1, 28	sylbi 195	. . . 4 $.\/$
30		simp313 1137	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	1, 30	sylbi 195	. . . 4 $.\/$
32	1	dalem-clpjq 33639	. . . 4 $.\/$
33	29, 31, 32	3jca 1168	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
34		simp322 1139	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	1, 34	sylbi 195	. . . 4 $.\/$
36		simp323 1140	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	1, 36	sylbi 195	. . . 4 $.\/$
38		simp321 1138	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39	1, 38	sylbi 195	. . . 4 $.\/$
40	35, 37, 39	3jca 1168	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
41	1	dalemclqjt 33637	. . . 4 $.\/$
42	1	dalemclrju 33638	. . . 4 $.\/$
43	1	dalemclpjs 33636	. . . 4 $.\/$
44	41, 42, 43	3jca 1168	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	33, 40, 44	3jca 1168	. 2 $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46	14, 27, 45	3jca 1168	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758 class class class wbr 4403

cfv 5529 (class class class)co 6203

cbs 14295

cple 14367

cjn 15236

catm 33266

chlt 33353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4514 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-op 3995 df-uni 4203 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-id 4747 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-poset 15238 df-lub 15266 df-glb 15267 df-join 15268 df-meet 15269 df-lat 15338 df-ats 33270 df-atl 33301 df-cvlat 33325 df-hlat 33354

This theorem is referenced by: dalemeea 33665 dalem6 33670 dalem7 33671 dalem11 33676 dalem12 33677 dalem29 33703 dalem30 33704 dalem31N 33705 dalem32 33706 dalem33 33707 dalem34 33708 dalem35 33709 dalem36 33710 dalem37 33711 dalem40 33714 dalem46 33720 dalem47 33721 dalem49 33723 dalem50 33724 dalem58 33732 dalem59 33733

W3C validator