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

Theorem cdleme50ldil 31346
 Description: Part of proof of Lemma D in [Crawley] p. 113. is a lattice dilation. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
Hypotheses
Ref Expression
cdlemef50.b
cdlemef50.l
cdlemef50.j
cdlemef50.m
cdlemef50.a
cdlemef50.h
cdlemef50.u
cdlemef50.d
cdlemefs50.e
cdlemef50.f
cdleme50ldil.i
Assertion
Ref Expression
cdleme50ldil
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,   ,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   (,,,,)   ()   (,)   (,,,,)

Proof of Theorem cdleme50ldil
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cdlemef50.b . . 3
2 cdlemef50.l . . 3
3 cdlemef50.j . . 3
4 cdlemef50.m . . 3
5 cdlemef50.a . . 3
6 cdlemef50.h . . 3
7 cdlemef50.u . . 3
8 cdlemef50.d . . 3
9 cdlemefs50.e . . 3
10 cdlemef50.f . . 3
11 eqid 2437 . . 3
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11cdleme50laut 31345 . 2
13 simpr 449 . . . . . . 7
1413con2i 115 . . . . . 6
1510cdleme31fv2 31191 . . . . . 6
1614, 15sylan2 462 . . . . 5
1716ex 425 . . . 4
1817rgen 2772 . . 3
1918a1i 11 . 2
20 cdleme50ldil.i . . . 4
211, 2, 6, 11, 20isldil 30908 . . 3