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

Theorem dihvalcqpre 31960
 Description: Value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 6-Mar-2014.)
Hypotheses
Ref Expression
dihval.b
dihval.l
dihval.j
dihval.m
dihval.a
dihval.h
dihval.i
dihval.d
dihval.c
dihval.u
dihval.s
dihval.p
Assertion
Ref Expression
dihvalcqpre

Proof of Theorem dihvalcqpre
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihval.s . . 3
2 fvex 5734 . . 3
31, 2eqeltri 2505 . 2
4 nfv 1629 . . 3
5 nfvd 1630 . . 3
6 dihval.b . . . . 5
7 dihval.l . . . . 5
8 dihval.j . . . . 5
9 dihval.m . . . . 5
10 dihval.a . . . . 5
11 dihval.h . . . . 5
12 dihval.i . . . . 5
13 dihval.d . . . . 5
14 dihval.c . . . . 5
15 dihval.u . . . . 5
16 dihval.p . . . . 5
176, 7, 8, 9, 10, 11, 12, 13, 14, 15, 1, 16dihvalc 31958 . . . 4
19 eqeq1 2441 . . . 4
21 simpl1 960 . . . . 5
22 simprl 733 . . . . . 6
23 simprrl 741 . . . . . 6
2422, 23jca 519 . . . . 5
25 simpl3l 1012 . . . . 5
26 simpl2l 1010 . . . . 5
27 simprrr 742 . . . . . 6
28 simpl3r 1013 . . . . . 6
2927, 28eqtr4d 2470 . . . . 5
306, 7, 8, 9, 10, 11, 13, 14, 15, 16dihjust 31942 . . . . 5
3121, 24, 25, 26, 29, 30syl131anc 1197 . . . 4
3231ex 424 . . 3
336, 7, 8, 9, 10, 11, 12, 13, 14, 15, 1, 16dihlsscpre 31959 . . . 4