Metamath Proof Explorer

Definition df-dih

Description: Define isomorphism H. (Contributed by NM, 28-Jan-2014)

Ref Expression
Assertion df-dih ⊢ DIsoH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdih class DIsoH
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 vx setvar x
8 cbs class Base
9 5 8 cfv class Base k
10 7 cv setvar x
11 cple class le
12 5 11 cfv class ≤ k
13 3 cv setvar w
14 10 13 12 wbr wff x ≤ k w
15 cdib class DIsoB
16 5 15 cfv class DIsoB ⁡ k
17 13 16 cfv class DIsoB ⁡ k ⁡ w
18 10 17 cfv class DIsoB ⁡ k ⁡ w ⁡ x
19 vu setvar u
20 clss class LSubSp
21 cdvh class DVecH
22 5 21 cfv class DVecH ⁡ k
23 13 22 cfv class DVecH ⁡ k ⁡ w
24 23 20 cfv class LSubSp ⁡ DVecH ⁡ k ⁡ w
25 vq setvar q
26 catm class Atoms
27 5 26 cfv class Atoms ⁡ k
28 25 cv setvar q
29 28 13 12 wbr wff q ≤ k w
30 29 wn wff ¬ q ≤ k w
31 cjn class join
32 5 31 cfv class join ⁡ k
33 cmee class meet
34 5 33 cfv class meet ⁡ k
35 10 13 34 co class x meet ⁡ k w
36 28 35 32 co class q join ⁡ k x meet ⁡ k w
37 36 10 wceq wff q join ⁡ k x meet ⁡ k w = x
38 30 37 wa wff ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x
39 19 cv setvar u
40 cdic class DIsoC
41 5 40 cfv class DIsoC ⁡ k
42 13 41 cfv class DIsoC ⁡ k ⁡ w
43 28 42 cfv class DIsoC ⁡ k ⁡ w ⁡ q
44 clsm class LSSum
45 23 44 cfv class LSSum ⁡ DVecH ⁡ k ⁡ w
46 35 17 cfv class DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
47 43 46 45 co class DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
48 39 47 wceq wff u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
49 38 48 wi wff ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
50 49 25 27 wral wff ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
51 50 19 24 crio class ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
52 14 18 51 cif class if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
53 7 9 52 cmpt class x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
54 3 6 53 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
55 1 2 54 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
56 0 55 wceq wff DIsoH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w