Metamath Proof Explorer

Definition df-dih

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

Ref Expression
Assertion df-dih ⊢DIsoH=k∈V⟼w∈LHyp⁡k⟼x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdih classDIsoH
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 vx setvarx
8 cbs classBase
9 5 8 cfv classBasek
10 7 cv setvarx
11 cple classle
12 5 11 cfv class≤k
13 3 cv setvarw
14 10 13 12 wbr wffx≤kw
15 cdib classDIsoB
16 5 15 cfv classDIsoB⁡k
17 13 16 cfv classDIsoB⁡k⁡w
18 10 17 cfv classDIsoB⁡k⁡w⁡x
19 vu setvaru
20 clss classLSubSp
21 cdvh classDVecH
22 5 21 cfv classDVecH⁡k
23 13 22 cfv classDVecH⁡k⁡w
24 23 20 cfv classLSubSp⁡DVecH⁡k⁡w
25 vq setvarq
26 catm classAtoms
27 5 26 cfv classAtoms⁡k
28 25 cv setvarq
29 28 13 12 wbr wffq≤kw
30 29 wn wff¬q≤kw
31 cjn classjoin
32 5 31 cfv classjoin⁡k
33 cmee classmeet
34 5 33 cfv classmeet⁡k
35 10 13 34 co classxmeet⁡kw
36 28 35 32 co classqjoin⁡kxmeet⁡kw
37 36 10 wceq wffqjoin⁡kxmeet⁡kw=x
38 30 37 wa wff¬q≤kw∧qjoin⁡kxmeet⁡kw=x
39 19 cv setvaru
40 cdic classDIsoC
41 5 40 cfv classDIsoC⁡k
42 13 41 cfv classDIsoC⁡k⁡w
43 28 42 cfv classDIsoC⁡k⁡w⁡q
44 clsm classLSSum
45 23 44 cfv classLSSum⁡DVecH⁡k⁡w
46 35 17 cfv classDIsoB⁡k⁡w⁡xmeet⁡kw
47 43 46 45 co classDIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
48 39 47 wceq wffu=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
49 38 48 wi wff¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
50 49 25 27 wral wff∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
51 50 19 24 crio classιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
52 14 18 51 cif classifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
53 7 9 52 cmpt classx∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
54 3 6 53 cmpt classw∈LHyp⁡k⟼x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
55 1 2 54 cmpt classk∈V⟼w∈LHyp⁡k⟼x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
56 0 55 wceq wffDIsoH=k∈V⟼w∈LHyp⁡k⟼x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw