trlval4 - Mathbox for Norm Megill

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

Theorem trlval4 33170

Description: The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-May-2013.)

**Hypotheses**
Ref	Expression
trlval3.l
trlval3.j	$.\/$
trlval3.m	$./\$
trlval3.a
trlval3.h
trlval3.t
trlval3.r

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

**Proof of Theorem trlval4**
Step	Hyp	Ref	Expression
1		simp1 995	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2		simp21 1028	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
3		simp22 1029	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
4		simp23 1030	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		simp3r 1024	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
6		simpl1l 1046	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
7		simp23l 1116	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8	7	adantr 463	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
9		simpl1 998	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
10		simpl21 1073	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
11		trlval3.l	. . . . . . . . . 10
12		trlval3.a	. . . . . . . . . 10
13		trlval3.h	. . . . . . . . . 10
14		trlval3.t	. . . . . . . . . 10
15	11, 12, 13, 14	ltrnat 33121	. . . . . . . . 9 $/\$ $/\$ $/\$
16	9, 10, 8, 15	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
17		trlval3.j	. . . . . . . . 9 $.\/$
18	11, 17, 12	hlatlej1 32356	. . . . . . . 8 $/\$ $/\$ $.\/$
19	6, 8, 16, 18	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
20		simpl22 1074	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
21		trlval3.r	. . . . . . . . . 10
22	11, 17, 12, 13, 14, 21	trljat1 33148	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
23	9, 10, 20, 22	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
24		simpr 459	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
25	23, 24	eqtrd 2441	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
26	19, 25	breqtrrd 4418	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
27		simpl3r 1051	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
28		simpll1 1034	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
29	20	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
30	10	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
31		simpr 459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
32		eqid 2400	. . . . . . . . . . . . . 14
33	11, 32, 12, 13, 14, 21	trl0 33152	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
34	28, 29, 30, 31, 33	syl112anc 1232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
35		hlatl 32342	. . . . . . . . . . . . . . 15
36	6, 35	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simp22l 1114	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
38	37	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39		eqid 2400	. . . . . . . . . . . . . . . 16
40	39, 17, 12	hlatjcl 32348	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
41	6, 38, 8, 40	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
42	39, 11, 32	atl0le 32286	. . . . . . . . . . . . . 14 $/\$ $.\/$ $.\/$
43	36, 41, 42	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
44	43	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
45	34, 44	eqbrtrd 4412	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
46	45	ex 432	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
47	46	necon3bd 2613	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
48	27, 47	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
49	11, 12, 13, 14, 21	trlat 33151	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
50	9, 20, 10, 48, 49	syl112anc 1232	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
51		simpl3l 1050	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
52	51	necomd 2672	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
53	11, 17, 12	hlatexch1 32376	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
54	6, 8, 50, 38, 52, 53	syl131anc 1241	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
55	26, 54	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
56	55	ex 432	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
57	56	necon3bd 2613	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
58	5, 57	mpd 15	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
59		trlval3.m	. . 3 $./\$
60	11, 17, 59, 12, 13, 14, 21	trlval3 33169	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
61	1, 2, 3, 4, 58, 60	syl113anc 1240	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 367 $/\$ w3a 972

wceq 1403

wcel 1840

wne 2596 class class class wbr 4392

cfv 5523 (class class class)co 6232

cbs 14731

cple 14806

cjn 15787

cmee 15788

cp0 15881

catm 32245

cal 32246

chlt 32332

clh 32965

cltrn 33082

ctrl 33140

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1637 ax-4 1650 ax-5 1723 ax-6 1769 ax-7 1812 ax-8 1842 ax-9 1844 ax-10 1859 ax-11 1864 ax-12 1876 ax-13 2024 ax-ext 2378 ax-rep 4504 ax-sep 4514 ax-nul 4522 ax-pow 4569 ax-pr 4627 ax-un 6528

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 974 df-tru 1406 df-ex 1632 df-nf 1636 df-sb 1762 df-eu 2240 df-mo 2241 df-clab 2386 df-cleq 2392 df-clel 2395 df-nfc 2550 df-ne 2598 df-ral 2756 df-rex 2757 df-reu 2758 df-rab 2760 df-v 3058 df-sbc 3275 df-csb 3371 df-dif 3414 df-un 3416 df-in 3418 df-ss 3425 df-nul 3736 df-if 3883 df-pw 3954 df-sn 3970 df-pr 3972 df-op 3976 df-uni 4189 df-iun 4270 df-iin 4271 df-br 4393 df-opab 4451 df-mpt 4452 df-id 4735 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5487 df-fun 5525 df-fn 5526 df-f 5527 df-f1 5528 df-fo 5529 df-f1o 5530 df-fv 5531 df-riota 6194 df-ov 6235 df-oprab 6236 df-mpt2 6237 df-1st 6736 df-2nd 6737 df-map 7377 df-preset 15771 df-poset 15789 df-plt 15802 df-lub 15818 df-glb 15819 df-join 15820 df-meet 15821 df-p0 15883 df-p1 15884 df-lat 15890 df-clat 15952 df-oposet 32158 df-ol 32160 df-oml 32161 df-covers 32248 df-ats 32249 df-atl 32280 df-cvlat 32304 df-hlat 32333 df-llines 32479 df-psubsp 32484 df-pmap 32485 df-padd 32777 df-lhyp 32969 df-laut 32970 df-ldil 33085 df-ltrn 33086 df-trl 33141

This theorem is referenced by: cdlemg10a 33623 cdlemg12d 33629

W3C validator