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 34190

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 988	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2		simp21 1021	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
3		simp22 1022	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
4		simp23 1023	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		simp3r 1017	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
6		simpl1l 1039	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
7		simp23l 1109	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8	7	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
9		simpl1 991	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
10		simpl21 1066	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
11		trlval3.l	. . . . . . . . . 10
12		trlval3.a	. . . . . . . . . 10
13		trlval3.h	. . . . . . . . . 10
14		trlval3.t	. . . . . . . . . 10
15	11, 12, 13, 14	ltrnat 34142	. . . . . . . . 9 $/\$ $/\$ $/\$
16	9, 10, 8, 15	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
17		trlval3.j	. . . . . . . . 9 $.\/$
18	11, 17, 12	hlatlej1 33377	. . . . . . . 8 $/\$ $/\$ $.\/$
19	6, 8, 16, 18	syl3anc 1219	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
20		simpl22 1067	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
21		trlval3.r	. . . . . . . . . 10
22	11, 17, 12, 13, 14, 21	trljat1 34168	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
23	9, 10, 20, 22	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
24		simpr 461	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
25	23, 24	eqtrd 2495	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
26	19, 25	breqtrrd 4429	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
27		simpl3r 1044	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
28		simpll1 1027	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
29	20	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$
30	10	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
31		simpr 461	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
32		eqid 2454	. . . . . . . . . . . . . 14
33	11, 32, 12, 13, 14, 21	trl0 34172	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
34	28, 29, 30, 31, 33	syl112anc 1223	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
35		hlatl 33363	. . . . . . . . . . . . . . 15
36	6, 35	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simp22l 1107	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
38	37	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39		eqid 2454	. . . . . . . . . . . . . . . 16
40	39, 17, 12	hlatjcl 33369	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
41	6, 38, 8, 40	syl3anc 1219	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
42	39, 11, 32	atl0le 33307	. . . . . . . . . . . . . 14 $/\$ $.\/$ $.\/$
43	36, 41, 42	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
44	43	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
45	34, 44	eqbrtrd 4423	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
46	45	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
47	46	necon3bd 2664	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
48	27, 47	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
49	11, 12, 13, 14, 21	trlat 34171	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
50	9, 20, 10, 48, 49	syl112anc 1223	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
51		simpl3l 1043	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
52	51	necomd 2723	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
53	11, 17, 12	hlatexch1 33397	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
54	6, 8, 50, 38, 52, 53	syl131anc 1232	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
55	26, 54	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
56	55	ex 434	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
57	56	necon3bd 2664	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
58	5, 57	mpd 15	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
59		trlval3.m	. . 3 $./\$
60	11, 17, 59, 12, 13, 14, 21	trlval3 34189	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
61	1, 2, 3, 4, 58, 60	syl113anc 1231	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wne 2648 class class class wbr 4403

cfv 5529 (class class class)co 6203

cbs 14295

cple 14367

cjn 15236

cmee 15237

cp0 15329

catm 33266

cal 33267

chlt 33353

clh 33986

cltrn 34103

ctrl 34160

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-iin 4285 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-mpt2 6208 df-1st 6690 df-2nd 6691 df-map 7329 df-poset 15238 df-plt 15250 df-lub 15266 df-glb 15267 df-join 15268 df-meet 15269 df-p0 15331 df-p1 15332 df-lat 15338 df-clat 15400 df-oposet 33179 df-ol 33181 df-oml 33182 df-covers 33269 df-ats 33270 df-atl 33301 df-cvlat 33325 df-hlat 33354 df-llines 33500 df-psubsp 33505 df-pmap 33506 df-padd 33798 df-lhyp 33990 df-laut 33991 df-ldil 34106 df-ltrn 34107 df-trl 34161

This theorem is referenced by: cdlemg10a 34642 cdlemg12d 34648

W3C validator