ltrnu - Mathbox for Norm Megill

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

Theorem ltrnu 33770

Description: Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom

. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 20-May-2012.)

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

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

Proof of Theorem ltrnu Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		an4 820	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simpr 461	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
3		simplr 754	. . . . . 6 $/\$ $/\$ $/\$ $/\$
4		ltrnu.l	. . . . . . . . 9
5		ltrnu.j	. . . . . . . . 9 $.\/$
6		ltrnu.m	. . . . . . . . 9 $./\$
7		ltrnu.a	. . . . . . . . 9
8		ltrnu.h	. . . . . . . . 9
9		eqid 2443	. . . . . . . . 9
10		ltrnu.t	. . . . . . . . 9
11	4, 5, 6, 7, 8, 9, 10	isltrn 33768	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
12	11	ad2antrr 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
13		simpr 461	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
14	12, 13	syl6bi 228	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
15	3, 14	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
16		breq1 4300	. . . . . . . . 9
17	16	notbid 294	. . . . . . . 8
18	17	anbi1d 704	. . . . . . 7 $/\$ $/\$
19		id 22	. . . . . . . . . 10
20		fveq2 5696	. . . . . . . . . 10
21	19, 20	oveq12d 6114	. . . . . . . . 9 $.\/$ $.\/$
22	21	oveq1d 6111	. . . . . . . 8 $.\/$ $./\$ $.\/$ $./\$
23	22	eqeq1d 2451	. . . . . . 7 $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$
24	18, 23	imbi12d 320	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
25		breq1 4300	. . . . . . . . 9
26	25	notbid 294	. . . . . . . 8
27	26	anbi2d 703	. . . . . . 7 $/\$ $/\$
28		id 22	. . . . . . . . . 10
29		fveq2 5696	. . . . . . . . . 10
30	28, 29	oveq12d 6114	. . . . . . . . 9 $.\/$ $.\/$
31	30	oveq1d 6111	. . . . . . . 8 $.\/$ $./\$ $.\/$ $./\$
32	31	eqeq2d 2454	. . . . . . 7 $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$
33	27, 32	imbi12d 320	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
34	24, 33	rspc2v 3084	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
35	2, 15, 34	sylc 60	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
36	35	impr 619	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
37	1, 36	sylan2b 475	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
38	37	3impb 1183	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wral 2720 class class class wbr 4297

cfv 5423 (class class class)co 6096

cple 14250

cjn 15119

cmee 15120

catm 32913

clh 33633

cldil 33749

cltrn 33750

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pr 4536

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-ral 2725 df-rex 2726 df-reu 2727 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-nul 3643 df-if 3797 df-sn 3883 df-pr 3885 df-op 3889 df-uni 4097 df-iun 4178 df-br 4298 df-opab 4356 df-mpt 4357 df-id 4641 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-ov 6099 df-ltrn 33754

This theorem is referenced by: ltrncnv 33795 trlval2 33812 cdlemg14f 34302 cdlemg14g 34303

W3C validator