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 40044
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 unity. 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 40043 . 2 class DIsoC
2 vk . . 3 setvar π‘˜
3 cvv 3475 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1541 . . . . 5 class π‘˜
6 clh 38855 . . . . 5 class LHyp
75, 6cfv 6544 . . . 4 class (LHypβ€˜π‘˜)
8 vq . . . . 5 setvar π‘ž
9 vr . . . . . . . . 9 setvar π‘Ÿ
109cv 1541 . . . . . . . 8 class π‘Ÿ
114cv 1541 . . . . . . . 8 class 𝑀
12 cple 17204 . . . . . . . . 9 class le
135, 12cfv 6544 . . . . . . . 8 class (leβ€˜π‘˜)
1410, 11, 13wbr 5149 . . . . . . 7 wff π‘Ÿ(leβ€˜π‘˜)𝑀
1514wn 3 . . . . . 6 wff Β¬ π‘Ÿ(leβ€˜π‘˜)𝑀
16 catm 38133 . . . . . . 7 class Atoms
175, 16cfv 6544 . . . . . 6 class (Atomsβ€˜π‘˜)
1815, 9, 17crab 3433 . . . . 5 class {π‘Ÿ ∈ (Atomsβ€˜π‘˜) ∣ Β¬ π‘Ÿ(leβ€˜π‘˜)𝑀}
19 vf . . . . . . . . 9 setvar 𝑓
2019cv 1541 . . . . . . . 8 class 𝑓
21 coc 17205 . . . . . . . . . . . . . 14 class oc
225, 21cfv 6544 . . . . . . . . . . . . 13 class (ocβ€˜π‘˜)
2311, 22cfv 6544 . . . . . . . . . . . 12 class ((ocβ€˜π‘˜)β€˜π‘€)
24 vg . . . . . . . . . . . . 13 setvar 𝑔
2524cv 1541 . . . . . . . . . . . 12 class 𝑔
2623, 25cfv 6544 . . . . . . . . . . 11 class (π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€))
278cv 1541 . . . . . . . . . . 11 class π‘ž
2826, 27wceq 1542 . . . . . . . . . 10 wff (π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž
29 cltrn 38972 . . . . . . . . . . . 12 class LTrn
305, 29cfv 6544 . . . . . . . . . . 11 class (LTrnβ€˜π‘˜)
3111, 30cfv 6544 . . . . . . . . . 10 class ((LTrnβ€˜π‘˜)β€˜π‘€)
3228, 24, 31crio 7364 . . . . . . . . 9 class (℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)
33 vs . . . . . . . . . 10 setvar 𝑠
3433cv 1541 . . . . . . . . 9 class 𝑠
3532, 34cfv 6544 . . . . . . . 8 class (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž))
3620, 35wceq 1542 . . . . . . 7 wff 𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž))
37 ctendo 39623 . . . . . . . . . 10 class TEndo
385, 37cfv 6544 . . . . . . . . 9 class (TEndoβ€˜π‘˜)
3911, 38cfv 6544 . . . . . . . 8 class ((TEndoβ€˜π‘˜)β€˜π‘€)
4034, 39wcel 2107 . . . . . . 7 wff 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€)
4136, 40wa 397 . . . . . 6 wff (𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)) ∧ 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€))
4241, 19, 33copab 5211 . . . . 5 class {βŸ¨π‘“, π‘ βŸ© ∣ (𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)) ∧ 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€))}
438, 18, 42cmpt 5232 . . . 4 class (π‘ž ∈ {π‘Ÿ ∈ (Atomsβ€˜π‘˜) ∣ Β¬ π‘Ÿ(leβ€˜π‘˜)𝑀} ↦ {βŸ¨π‘“, π‘ βŸ© ∣ (𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)) ∧ 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€))})
444, 7, 43cmpt 5232 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘ž ∈ {π‘Ÿ ∈ (Atomsβ€˜π‘˜) ∣ Β¬ π‘Ÿ(leβ€˜π‘˜)𝑀} ↦ {βŸ¨π‘“, π‘ βŸ© ∣ (𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)) ∧ 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€))}))
452, 3, 44cmpt 5232 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘ž ∈ {π‘Ÿ ∈ (Atomsβ€˜π‘˜) ∣ Β¬ π‘Ÿ(leβ€˜π‘˜)𝑀} ↦ {βŸ¨π‘“, π‘ βŸ© ∣ (𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)) ∧ 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€))})))
461, 45wceq 1542 1 wff DIsoC = (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ (π‘ž ∈ {π‘Ÿ ∈ (Atomsβ€˜π‘˜) ∣ Β¬ π‘Ÿ(leβ€˜π‘˜)𝑀} ↦ {βŸ¨π‘“, π‘ βŸ© ∣ (𝑓 = (π‘ β€˜(℩𝑔 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘”β€˜((ocβ€˜π‘˜)β€˜π‘€)) = π‘ž)) ∧ 𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€))})))
Colors of variables: wff setvar class
This definition is referenced by:  dicffval  40045
  Copyright terms: Public domain W3C validator