Definition df-dic 41116

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

Step	Hyp	Ref	Expression
1		cdic 41115	. 2 class DIsoC
2		vk	. . 3 setvar 𝑘
3		cvv 3464	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 39927	. . . . 5 class LHyp
7	5, 6	cfv 6542	. . . 4 class (LHyp‘𝑘)
8		vq	. . . . 5 setvar 𝑞
9		vr	. . . . . . . . 9 setvar 𝑟
10	9	cv 1538	. . . . . . . 8 class 𝑟
11	4	cv 1538	. . . . . . . 8 class 𝑤
12		cple 17284	. . . . . . . . 9 class le
13	5, 12	cfv 6542	. . . . . . . 8 class (le‘𝑘)
14	10, 11, 13	wbr 5125	. . . . . . 7 wff 𝑟(le‘𝑘)𝑤
15	14	wn 3	. . . . . 6 wff ¬ 𝑟(le‘𝑘)𝑤
16		catm 39205	. . . . . . 7 class Atoms
17	5, 16	cfv 6542	. . . . . 6 class (Atoms‘𝑘)
18	15, 9, 17	crab 3420	. . . . 5 class {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤}
19		vf	. . . . . . . . 9 setvar 𝑓
20	19	cv 1538	. . . . . . . 8 class 𝑓
21		coc 17285	. . . . . . . . . . . . . 14 class oc
22	5, 21	cfv 6542	. . . . . . . . . . . . 13 class (oc‘𝑘)
23	11, 22	cfv 6542	. . . . . . . . . . . 12 class ((oc‘𝑘)‘𝑤)
24		vg	. . . . . . . . . . . . 13 setvar 𝑔
25	24	cv 1538	. . . . . . . . . . . 12 class 𝑔
26	23, 25	cfv 6542	. . . . . . . . . . 11 class (𝑔‘((oc‘𝑘)‘𝑤))
27	8	cv 1538	. . . . . . . . . . 11 class 𝑞
28	26, 27	wceq 1539	. . . . . . . . . 10 wff (𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞
29		cltrn 40044	. . . . . . . . . . . 12 class LTrn
30	5, 29	cfv 6542	. . . . . . . . . . 11 class (LTrn‘𝑘)
31	11, 30	cfv 6542	. . . . . . . . . 10 class ((LTrn‘𝑘)‘𝑤)
32	28, 24, 31	crio 7370	. . . . . . . . 9 class (℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)
33		vs	. . . . . . . . . 10 setvar 𝑠
34	33	cv 1538	. . . . . . . . 9 class 𝑠
35	32, 34	cfv 6542	. . . . . . . 8 class (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞))
36	20, 35	wceq 1539	. . . . . . 7 wff 𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞))
37		ctendo 40695	. . . . . . . . . 10 class TEndo
38	5, 37	cfv 6542	. . . . . . . . 9 class (TEndo‘𝑘)
39	11, 38	cfv 6542	. . . . . . . 8 class ((TEndo‘𝑘)‘𝑤)
40	34, 39	wcel 2107	. . . . . . 7 wff 𝑠 ∈ ((TEndo‘𝑘)‘𝑤)
41	36, 40	wa 395	. . . . . 6 wff (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))
42	41, 19, 33	copab 5187	. . . . 5 class {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}
43	8, 18, 42	cmpt 5207	. . . 4 class (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})
44	4, 7, 43	cmpt 5207	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}))
45	2, 3, 44	cmpt 5207	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})))
46	1, 45	wceq 1539	1 wff DIsoC = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})))

This definition is referenced by:  dicffval  41117