This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑘 ∈ 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 ‘ 𝑘 ) ‘ 𝑤 ) ) } ) ) )