Metamath Proof Explorer

Definition df-dih

Description: Define isomorphism H. (Contributed by NM, 28-Jan-2014)

Ref Expression
Assertion df-dih 
|- DIsoH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdih 
 |-  DIsoH
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vx 
 |-  x
8 cbs 
 |-  Base
9 5 8 cfv 
 |-  ( Base ` k )
10 7 cv 
 |-  x
11 cple 
 |-  le
12 5 11 cfv 
 |-  ( le ` k )
13 3 cv 
 |-  w
14 10 13 12 wbr 
 |-  x ( le ` k ) w
15 cdib 
 |-  DIsoB
16 5 15 cfv 
 |-  ( DIsoB ` k )
17 13 16 cfv 
 |-  ( ( DIsoB ` k ) ` w )
18 10 17 cfv 
 |-  ( ( ( DIsoB ` k ) ` w ) ` x )
19 vu 
 |-  u
20 clss 
 |-  LSubSp
21 cdvh 
 |-  DVecH
22 5 21 cfv 
 |-  ( DVecH ` k )
23 13 22 cfv 
 |-  ( ( DVecH ` k ) ` w )
24 23 20 cfv 
 |-  ( LSubSp ` ( ( DVecH ` k ) ` w ) )
25 vq 
 |-  q
26 catm 
 |-  Atoms
27 5 26 cfv 
 |-  ( Atoms ` k )
28 25 cv 
 |-  q
29 28 13 12 wbr 
 |-  q ( le ` k ) w
30 29 wn 
 |-  -. q ( le ` k ) w
31 cjn 
 |-  join
32 5 31 cfv 
 |-  ( join ` k )
33 cmee 
 |-  meet
34 5 33 cfv 
 |-  ( meet ` k )
35 10 13 34 co 
 |-  ( x ( meet ` k ) w )
36 28 35 32 co 
 |-  ( q ( join ` k ) ( x ( meet ` k ) w ) )
37 36 10 wceq 
 |-  ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x
38 30 37 wa 
 |-  ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x )
39 19 cv 
 |-  u
40 cdic 
 |-  DIsoC
41 5 40 cfv 
 |-  ( DIsoC ` k )
42 13 41 cfv 
 |-  ( ( DIsoC ` k ) ` w )
43 28 42 cfv 
 |-  ( ( ( DIsoC ` k ) ` w ) ` q )
44 clsm 
 |-  LSSum
45 23 44 cfv 
 |-  ( LSSum ` ( ( DVecH ` k ) ` w ) )
46 35 17 cfv 
 |-  ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) )
47 43 46 45 co 
 |-  ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) )
48 39 47 wceq 
 |-  u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) )
49 38 48 wi 
 |-  ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) )
50 49 25 27 wral 
 |-  A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) )
51 50 19 24 crio 
 |-  ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) )
52 14 18 51 cif 
 |-  if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) )
53 7 9 52 cmpt 
 |-  ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) )
54 3 6 53 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) )
55 1 2 54 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) ) )
56 0 55 wceq 
 |-  DIsoH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) ) )