dalemrot - Mathbox for Norm Megill

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

Theorem dalemrot 33293

Description: Lemma for dath 33372. 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 33259	. . . 4
3		dalemc.a	. . . . 5
4	1, 3	dalemceb 33274	. . . 4
5	2, 4	jca 541	. . 3 $/\$
6	1	dalemqea 33263	. . . 4
7	1	dalemrea 33264	. . . 4
8	1	dalempea 33262	. . . 4
9	6, 7, 8	3jca 1210	. . 3 $/\$ $/\$
10	1	dalemtea 33266	. . . 4
11	1	dalemuea 33267	. . . 4
12	1	dalemsea 33265	. . . 4
13	10, 11, 12	3jca 1210	. . 3 $/\$ $/\$
14	5, 9, 13	3jca 1210	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		dalemc.j	. . . . 5 $.\/$
16	1, 15, 3	dalemqrprot 33284	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
17		dalemrot.y	. . . . 5 $.\/$ $.\/$
18	1	dalemyeo 33268	. . . . 5
19	17, 18	syl5eqelr 2554	. . . 4 $.\/$ $.\/$
20	16, 19	eqeltrd 2549	. . 3 $.\/$ $.\/$
21	15, 3	hlatjrot 33009	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	2, 10, 11, 12, 21	syl13anc 1294	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
23		dalemrot.z	. . . . 5 $.\/$ $.\/$
24	1	dalemzeo 33269	. . . . 5
25	23, 24	syl5eqelr 2554	. . . 4 $.\/$ $.\/$
26	22, 25	eqeltrd 2549	. . 3 $.\/$ $.\/$
27	20, 26	jca 541	. 2 $.\/$ $.\/$ $/\$ $.\/$ $.\/$
28		simp312 1178	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
29	1, 28	sylbi 200	. . . 4 $.\/$
30		simp313 1179	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	1, 30	sylbi 200	. . . 4 $.\/$
32	1	dalem-clpjq 33273	. . . 4 $.\/$
33	29, 31, 32	3jca 1210	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
34		simp322 1181	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	1, 34	sylbi 200	. . . 4 $.\/$
36		simp323 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	1, 36	sylbi 200	. . . 4 $.\/$
38		simp321 1180	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39	1, 38	sylbi 200	. . . 4 $.\/$
40	35, 37, 39	3jca 1210	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
41	1	dalemclqjt 33271	. . . 4 $.\/$
42	1	dalemclrju 33272	. . . 4 $.\/$
43	1	dalemclpjs 33270	. . . 4 $.\/$
44	41, 42, 43	3jca 1210	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	33, 40, 44	3jca 1210	. 2 $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46	14, 27, 45	3jca 1210	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904 class class class wbr 4395

cfv 5589 (class class class)co 6308

cbs 15199

cple 15275

cjn 16267

catm 32900

chlt 32987

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-preset 16251 df-poset 16269 df-lub 16298 df-glb 16299 df-join 16300 df-meet 16301 df-lat 16370 df-ats 32904 df-atl 32935 df-cvlat 32959 df-hlat 32988

This theorem is referenced by: dalemeea 33299 dalem6 33304 dalem7 33305 dalem11 33310 dalem12 33311 dalem29 33337 dalem30 33338 dalem31N 33339 dalem32 33340 dalem33 33341 dalem34 33342 dalem35 33343 dalem36 33344 dalem37 33345 dalem40 33348 dalem46 33354 dalem47 33355 dalem49 33357 dalem50 33358 dalem58 33366 dalem59 33367

W3C validator