ltrnu - Mathbox for Norm Megill

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

Theorem ltrnu 33698

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 834	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simpr 463	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
3		simplr 763	. . . . . 6 $/\$ $/\$ $/\$ $/\$
4		ltrnu.l	. . . . . . . . 9
5		ltrnu.j	. . . . . . . . 9 $.\/$
6		ltrnu.m	. . . . . . . . 9 $./\$
7		ltrnu.a	. . . . . . . . 9
8		ltrnu.h	. . . . . . . . 9
9		eqid 2453	. . . . . . . . 9
10		ltrnu.t	. . . . . . . . 9
11	4, 5, 6, 7, 8, 9, 10	isltrn 33696	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
12	11	ad2antrr 733	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
13		simpr 463	. . . . . . 7 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
14	12, 13	syl6bi 232	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
15	3, 14	mpd 15	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
16		breq1 4408	. . . . . . . . 9
17	16	notbid 296	. . . . . . . 8
18	17	anbi1d 712	. . . . . . 7 $/\$ $/\$
19		id 22	. . . . . . . . . 10
20		fveq2 5870	. . . . . . . . . 10
21	19, 20	oveq12d 6313	. . . . . . . . 9 $.\/$ $.\/$
22	21	oveq1d 6310	. . . . . . . 8 $.\/$ $./\$ $.\/$ $./\$
23	22	eqeq1d 2455	. . . . . . 7 $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$
24	18, 23	imbi12d 322	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
25		breq1 4408	. . . . . . . . 9
26	25	notbid 296	. . . . . . . 8
27	26	anbi2d 711	. . . . . . 7 $/\$ $/\$
28		id 22	. . . . . . . . . 10
29		fveq2 5870	. . . . . . . . . 10
30	28, 29	oveq12d 6313	. . . . . . . . 9 $.\/$ $.\/$
31	30	oveq1d 6310	. . . . . . . 8 $.\/$ $./\$ $.\/$ $./\$
32	31	eqeq2d 2463	. . . . . . 7 $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$
33	27, 32	imbi12d 322	. . . . . 6 $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
34	24, 33	rspc2v 3161	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
35	2, 15, 34	sylc 62	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
36	35	impr 625	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
37	1, 36	sylan2b 478	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
38	37	3impb 1205	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1446

wcel 1889

wral 2739 class class class wbr 4405

cfv 5585 (class class class)co 6295

cple 15209

cjn 16201

cmee 16202

catm 32841

clh 33561

cldil 33677

cltrn 33678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pr 4642

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-reu 2746 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-ov 6298 df-ltrn 33682

This theorem is referenced by: ltrncnv 33723 trlval2 33741 cdlemg14f 34232 cdlemg14g 34233

W3C validator