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 = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ q ∈ r ∈ Atoms ⁡ k | ¬ r ≤ k w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdic class DIsoC
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vq setvar q
8 vr setvar r
9 catm class Atoms
10 5 9 cfv class Atoms ⁡ k
11 8 cv setvar r
12 cple class le
13 5 12 cfv class ≤ k
14 3 cv setvar w
15 11 14 13 wbr wff r ≤ k w
16 15 wn wff ¬ r ≤ k w
17 16 8 10 crab class r ∈ Atoms ⁡ k | ¬ r ≤ k w
18 vf setvar f
19 vs setvar s
20 18 cv setvar f
21 19 cv setvar s
22 vg setvar g
23 cltrn class LTrn
24 5 23 cfv class LTrn ⁡ k
25 14 24 cfv class LTrn ⁡ k ⁡ w
26 22 cv setvar g
27 coc class oc
28 5 27 cfv class oc ⁡ k
29 14 28 cfv class oc ⁡ k ⁡ w
30 29 26 cfv class g ⁡ oc ⁡ k ⁡ w
31 7 cv setvar q
32 30 31 wceq wff g ⁡ oc ⁡ k ⁡ w = q
33 32 22 25 crio class ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q
34 33 21 cfv class s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q
35 20 34 wceq wff f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q
36 ctendo class TEndo
37 5 36 cfv class TEndo ⁡ k
38 14 37 cfv class TEndo ⁡ k ⁡ w
39 21 38 wcel wff s ∈ TEndo ⁡ k ⁡ w
40 35 39 wa wff f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w
41 40 18 19 copab class f s | f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w
42 7 17 41 cmpt class q ∈ r ∈ Atoms ⁡ k | ¬ r ≤ k w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w
43 3 6 42 cmpt class w ∈ LHyp ⁡ k ⟼ q ∈ r ∈ Atoms ⁡ k | ¬ r ≤ k w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w
44 1 2 43 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ q ∈ r ∈ Atoms ⁡ k | ¬ r ≤ k w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w
45 0 44 wceq wff DIsoC = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ q ∈ r ∈ Atoms ⁡ k | ¬ r ≤ k w ⟼ f s | f = s ⁡ ι g ∈ LTrn ⁡ k ⁡ w | g ⁡ oc ⁡ k ⁡ w = q ∧ s ∈ TEndo ⁡ k ⁡ w