Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dic Structured version   Visualization version   GIF version

Definition df-dic 35276
Description: Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom 𝑤. The value is a one-dimensional subspace generated by the pair consisting of the vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom ((oc k ) 𝑤) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.)
Assertion
Ref Expression
df-dic DIsoC = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})))
Distinct variable group:   𝑤,𝑘,𝑞,𝑟,𝑓,𝑠,𝑔

Detailed syntax breakdown of Definition df-dic
StepHypRef Expression
1 cdic 35275 . 2 class DIsoC
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1473 . . . . 5 class 𝑘
6 clh 34084 . . . . 5 class LHyp
75, 6cfv 5790 . . . 4 class (LHyp‘𝑘)
8 vq . . . . 5 setvar 𝑞
9 vr . . . . . . . . 9 setvar 𝑟
109cv 1473 . . . . . . . 8 class 𝑟
114cv 1473 . . . . . . . 8 class 𝑤
12 cple 15721 . . . . . . . . 9 class le
135, 12cfv 5790 . . . . . . . 8 class (le‘𝑘)
1410, 11, 13wbr 4577 . . . . . . 7 wff 𝑟(le‘𝑘)𝑤
1514wn 3 . . . . . 6 wff ¬ 𝑟(le‘𝑘)𝑤
16 catm 33364 . . . . . . 7 class Atoms
175, 16cfv 5790 . . . . . 6 class (Atoms‘𝑘)
1815, 9, 17crab 2899 . . . . 5 class {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤}
19 vf . . . . . . . . 9 setvar 𝑓
2019cv 1473 . . . . . . . 8 class 𝑓
21 coc 15722 . . . . . . . . . . . . . 14 class oc
225, 21cfv 5790 . . . . . . . . . . . . 13 class (oc‘𝑘)
2311, 22cfv 5790 . . . . . . . . . . . 12 class ((oc‘𝑘)‘𝑤)
24 vg . . . . . . . . . . . . 13 setvar 𝑔
2524cv 1473 . . . . . . . . . . . 12 class 𝑔
2623, 25cfv 5790 . . . . . . . . . . 11 class (𝑔‘((oc‘𝑘)‘𝑤))
278cv 1473 . . . . . . . . . . 11 class 𝑞
2826, 27wceq 1474 . . . . . . . . . 10 wff (𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞
29 cltrn 34201 . . . . . . . . . . . 12 class LTrn
305, 29cfv 5790 . . . . . . . . . . 11 class (LTrn‘𝑘)
3111, 30cfv 5790 . . . . . . . . . 10 class ((LTrn‘𝑘)‘𝑤)
3228, 24, 31crio 6488 . . . . . . . . 9 class (𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)
33 vs . . . . . . . . . 10 setvar 𝑠
3433cv 1473 . . . . . . . . 9 class 𝑠
3532, 34cfv 5790 . . . . . . . 8 class (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞))
3620, 35wceq 1474 . . . . . . 7 wff 𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞))
37 ctendo 34854 . . . . . . . . . 10 class TEndo
385, 37cfv 5790 . . . . . . . . 9 class (TEndo‘𝑘)
3911, 38cfv 5790 . . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
4034, 39wcel 1976 . . . . . . 7 wff 𝑠 ∈ ((TEndo‘𝑘)‘𝑤)
4136, 40wa 382 . . . . . 6 wff (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))
4241, 19, 33copab 4636 . . . . 5 class {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}
438, 18, 42cmpt 4637 . . . 4 class (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})
444, 7, 43cmpt 4637 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}))
452, 3, 44cmpt 4637 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})))
461, 45wceq 1474 1 wff DIsoC = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})))
Colors of variables: wff setvar class
This definition is referenced by:  dicffval  35277
  Copyright terms: Public domain W3C validator