Definition df-dih 35536

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

Assertion

Ref	Expression
df-dih	⊢ DIsoH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))))

Distinct variable group:   𝑘,𝑞,𝑤,𝑢,𝑥

Detailed syntax breakdown of Definition df-dih

Step	Hyp	Ref	Expression
1		cdih 35535	. 2 class DIsoH
2		vk	. . 3 setvar 𝑘
3		cvv 3173	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1474	. . . . 5 class 𝑘
6		clh 34288	. . . . 5 class LHyp
7	5, 6	cfv 5804	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9		cbs 15695	. . . . . 6 class Base
10	5, 9	cfv 5804	. . . . 5 class (Base‘𝑘)
11	8	cv 1474	. . . . . . 7 class 𝑥
12	4	cv 1474	. . . . . . 7 class 𝑤
13		cple 15775	. . . . . . . 8 class le
14	5, 13	cfv 5804	. . . . . . 7 class (le‘𝑘)
15	11, 12, 14	wbr 4583	. . . . . 6 wff 𝑥(le‘𝑘)𝑤
16		cdib 35445	. . . . . . . . 9 class DIsoB
17	5, 16	cfv 5804	. . . . . . . 8 class (DIsoB‘𝑘)
18	12, 17	cfv 5804	. . . . . . 7 class ((DIsoB‘𝑘)‘𝑤)
19	11, 18	cfv 5804	. . . . . 6 class (((DIsoB‘𝑘)‘𝑤)‘𝑥)
20		vq	. . . . . . . . . . . . 13 setvar 𝑞
21	20	cv 1474	. . . . . . . . . . . 12 class 𝑞
22	21, 12, 14	wbr 4583	. . . . . . . . . . 11 wff 𝑞(le‘𝑘)𝑤
23	22	wn 3	. . . . . . . . . 10 wff ¬ 𝑞(le‘𝑘)𝑤
24		cmee 16768	. . . . . . . . . . . . . 14 class meet
25	5, 24	cfv 5804	. . . . . . . . . . . . 13 class (meet‘𝑘)
26	11, 12, 25	co 6549	. . . . . . . . . . . 12 class (𝑥(meet‘𝑘)𝑤)
27		cjn 16767	. . . . . . . . . . . . 13 class join
28	5, 27	cfv 5804	. . . . . . . . . . . 12 class (join‘𝑘)
29	21, 26, 28	co 6549	. . . . . . . . . . 11 class (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤))
30	29, 11	wceq 1475	. . . . . . . . . 10 wff (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥
31	23, 30	wa 383	. . . . . . . . 9 wff (¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥)
32		vu	. . . . . . . . . . 11 setvar 𝑢
33	32	cv 1474	. . . . . . . . . 10 class 𝑢
34		cdic 35479	. . . . . . . . . . . . . 14 class DIsoC
35	5, 34	cfv 5804	. . . . . . . . . . . . 13 class (DIsoC‘𝑘)
36	12, 35	cfv 5804	. . . . . . . . . . . 12 class ((DIsoC‘𝑘)‘𝑤)
37	21, 36	cfv 5804	. . . . . . . . . . 11 class (((DIsoC‘𝑘)‘𝑤)‘𝑞)
38	26, 18	cfv 5804	. . . . . . . . . . 11 class (((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))
39		cdvh 35385	. . . . . . . . . . . . . 14 class DVecH
40	5, 39	cfv 5804	. . . . . . . . . . . . 13 class (DVecH‘𝑘)
41	12, 40	cfv 5804	. . . . . . . . . . . 12 class ((DVecH‘𝑘)‘𝑤)
42		clsm 17872	. . . . . . . . . . . 12 class LSSum
43	41, 42	cfv 5804	. . . . . . . . . . 11 class (LSSum‘((DVecH‘𝑘)‘𝑤))
44	37, 38, 43	co 6549	. . . . . . . . . 10 class ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))
45	33, 44	wceq 1475	. . . . . . . . 9 wff 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))
46	31, 45	wi 4	. . . . . . . 8 wff ((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))))
47		catm 33568	. . . . . . . . 9 class Atoms
48	5, 47	cfv 5804	. . . . . . . 8 class (Atoms‘𝑘)
49	46, 20, 48	wral 2896	. . . . . . 7 wff ∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))))
50		clss 18753	. . . . . . . 8 class LSubSp
51	41, 50	cfv 5804	. . . . . . 7 class (LSubSp‘((DVecH‘𝑘)‘𝑤))
52	49, 32, 51	crio 6510	. . . . . 6 class (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))
53	15, 19, 52	cif 4036	. . . . 5 class if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))))))
54	8, 10, 53	cmpt 4643	. . . 4 class (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))
55	4, 7, 54	cmpt 4643	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤))))))))
56	2, 3, 55	cmpt 4643	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))))
57	1, 56	wceq 1475	1 wff DIsoH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ (Base‘𝑘) ↦ if(𝑥(le‘𝑘)𝑤, (((DIsoB‘𝑘)‘𝑤)‘𝑥), (℩𝑢 ∈ (LSubSp‘((DVecH‘𝑘)‘𝑤))∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑞(le‘𝑘)𝑤 ∧ (𝑞(join‘𝑘)(𝑥(meet‘𝑘)𝑤)) = 𝑥) → 𝑢 = ((((DIsoC‘𝑘)‘𝑤)‘𝑞)(LSSum‘((DVecH‘𝑘)‘𝑤))(((DIsoB‘𝑘)‘𝑤)‘(𝑥(meet‘𝑘)𝑤)))))))))

This definition is referenced by:  dihffval  35537