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 33222

Description: Lemma for dath 33301. 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 33188	. . . 4
3		dalemc.a	. . . . 5
4	1, 3	dalemceb 33203	. . . 4
5	2, 4	jca 535	. . 3 $/\$
6	1	dalemqea 33192	. . . 4
7	1	dalemrea 33193	. . . 4
8	1	dalempea 33191	. . . 4
9	6, 7, 8	3jca 1188	. . 3 $/\$ $/\$
10	1	dalemtea 33195	. . . 4
11	1	dalemuea 33196	. . . 4
12	1	dalemsea 33194	. . . 4
13	10, 11, 12	3jca 1188	. . 3 $/\$ $/\$
14	5, 9, 13	3jca 1188	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		dalemc.j	. . . . 5 $.\/$
16	1, 15, 3	dalemqrprot 33213	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
17		dalemrot.y	. . . . 5 $.\/$ $.\/$
18	1	dalemyeo 33197	. . . . 5
19	17, 18	syl5eqelr 2534	. . . 4 $.\/$ $.\/$
20	16, 19	eqeltrd 2529	. . 3 $.\/$ $.\/$
21	15, 3	hlatjrot 32938	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	2, 10, 11, 12, 21	syl13anc 1270	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
23		dalemrot.z	. . . . 5 $.\/$ $.\/$
24	1	dalemzeo 33198	. . . . 5
25	23, 24	syl5eqelr 2534	. . . 4 $.\/$ $.\/$
26	22, 25	eqeltrd 2529	. . 3 $.\/$ $.\/$
27	20, 26	jca 535	. 2 $.\/$ $.\/$ $/\$ $.\/$ $.\/$
28		simp312 1156	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
29	1, 28	sylbi 199	. . . 4 $.\/$
30		simp313 1157	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	1, 30	sylbi 199	. . . 4 $.\/$
32	1	dalem-clpjq 33202	. . . 4 $.\/$
33	29, 31, 32	3jca 1188	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
34		simp322 1159	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	1, 34	sylbi 199	. . . 4 $.\/$
36		simp323 1160	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	1, 36	sylbi 199	. . . 4 $.\/$
38		simp321 1158	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39	1, 38	sylbi 199	. . . 4 $.\/$
40	35, 37, 39	3jca 1188	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
41	1	dalemclqjt 33200	. . . 4 $.\/$
42	1	dalemclrju 33201	. . . 4 $.\/$
43	1	dalemclpjs 33199	. . . 4 $.\/$
44	41, 42, 43	3jca 1188	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	33, 40, 44	3jca 1188	. 2 $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46	14, 27, 45	3jca 1188	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887 class class class wbr 4402

cfv 5582 (class class class)co 6290

cbs 15121

cple 15197

cjn 16189

catm 32829

chlt 32916

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-preset 16173 df-poset 16191 df-lub 16220 df-glb 16221 df-join 16222 df-meet 16223 df-lat 16292 df-ats 32833 df-atl 32864 df-cvlat 32888 df-hlat 32917

This theorem is referenced by: dalemeea 33228 dalem6 33233 dalem7 33234 dalem11 33239 dalem12 33240 dalem29 33266 dalem30 33267 dalem31N 33268 dalem32 33269 dalem33 33270 dalem34 33271 dalem35 33272 dalem36 33273 dalem37 33274 dalem40 33277 dalem46 33283 dalem47 33284 dalem49 33286 dalem50 33287 dalem58 33295 dalem59 33296

W3C validator