Metamath Proof Explorer

Definition df-dic

Description: Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom w . The value is a one-dimensional subspace generated by the pair consisting of the iota_ vector below and the endomorphism ring unity. Definition of phi(q) in Crawley p. 121. Note that we use the fixed atom ( ( oc k ) w ) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013)

Ref Expression
Assertion df-dic ⊢DIsoC=k∈V⟼w∈LHyp⁡k⟼q∈r∈Atoms⁡k|¬r≤kw⟼fs|f=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdic classDIsoC
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 vq setvarq
8 vr setvarr
9 catm classAtoms
10 5 9 cfv classAtoms⁡k
11 8 cv setvarr
12 cple classle
13 5 12 cfv class≤k
14 3 cv setvarw
15 11 14 13 wbr wffr≤kw
16 15 wn wff¬r≤kw
17 16 8 10 crab classr∈Atoms⁡k|¬r≤kw
18 vf setvarf
19 vs setvars
20 18 cv setvarf
21 19 cv setvars
22 vg setvarg
23 cltrn classLTrn
24 5 23 cfv classLTrn⁡k
25 14 24 cfv classLTrn⁡k⁡w
26 22 cv setvarg
27 coc classoc
28 5 27 cfv classoc⁡k
29 14 28 cfv classoc⁡k⁡w
30 29 26 cfv classg⁡oc⁡k⁡w
31 7 cv setvarq
32 30 31 wceq wffg⁡oc⁡k⁡w=q
33 32 22 25 crio classιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q
34 33 21 cfv classs⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q
35 20 34 wceq wfff=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q
36 ctendo classTEndo
37 5 36 cfv classTEndo⁡k
38 14 37 cfv classTEndo⁡k⁡w
39 21 38 wcel wffs∈TEndo⁡k⁡w
40 35 39 wa wfff=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w
41 40 18 19 copab classfs|f=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w
42 7 17 41 cmpt classq∈r∈Atoms⁡k|¬r≤kw⟼fs|f=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w
43 3 6 42 cmpt classw∈LHyp⁡k⟼q∈r∈Atoms⁡k|¬r≤kw⟼fs|f=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w
44 1 2 43 cmpt classk∈V⟼w∈LHyp⁡k⟼q∈r∈Atoms⁡k|¬r≤kw⟼fs|f=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w
45 0 44 wceq wffDIsoC=k∈V⟼w∈LHyp⁡k⟼q∈r∈Atoms⁡k|¬r≤kw⟼fs|f=s⁡ιg∈LTrn⁡k⁡w|g⁡oc⁡k⁡w=q∧s∈TEndo⁡k⁡w