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 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑞 ∈ { 𝑟 ∈ ( Atoms ‘ 𝑘 ) ∣ ¬ 𝑟 ( le ‘ 𝑘 ) 𝑤 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑔 ‘ ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) = 𝑞 ) ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ) )

Detailed syntax breakdown

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