Theorem dihfval

Description: Isomorphism H for a lattice K . Definition of isomorphism map in Crawley p. 122 line 3. (Contributed by NM, 28-Jan-2014)

	Ref	Expression
Hypotheses	dihval.b	$$⊢B={\mathrm{Base}}_K$$
	dihval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihval.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihval.d	$$⊢D=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
	dihval.c	$$⊢C=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
	dihval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihval.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dihval.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
Assertion	dihfval	$$⊢\left(K\in V\wedge W\in H\right)\to I=\left(x\in B⟼if\left(x\underset{\dot{}}{\le }W,D\left(x\right),\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihval.b	$$⊢B={\mathrm{Base}}_K$$
2		dihval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		dihval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		dihval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		dihval.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
8		dihval.d	$$⊢D=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
9		dihval.c	$$⊢C=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
10		dihval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
11		dihval.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
12		dihval.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
13	1 2 3 4 5 6	dihffval	$$⊢K\in V\to \mathrm{DIsoH}\left(K\right)=\left(w\in H⟼\left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)\right)$$
14	13	fveq1d	$$⊢K\in V\to \mathrm{DIsoH}\left(K\right)\left(W\right)=\left(w\in H⟼\left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)\right)\left(W\right)$$
15	7 14	syl5eq	$$⊢K\in V\to I=\left(w\in H⟼\left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)\right)\left(W\right)$$
16		breq2	$$⊢w=W\to \left(x\underset{\dot{}}{\le }w\leftrightarrow x\underset{\dot{}}{\le }W\right)$$
17		fveq2	$$⊢w=W\to \mathrm{DIsoB}\left(K\right)\left(w\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
18	17 8	syl6eqr	$$⊢w=W\to \mathrm{DIsoB}\left(K\right)\left(w\right)=D$$
19	18	fveq1d	$$⊢w=W\to \mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right)=D\left(x\right)$$
20		fveq2	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
21	20 10	syl6eqr	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=U$$
22	21	fveq2d	$$⊢w=W\to \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)=\mathrm{LSubSp}\left(U\right)$$
23	22 11	syl6eqr	$$⊢w=W\to \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)=S$$
24		breq2	$$⊢w=W\to \left(q\underset{\dot{}}{\le }w\leftrightarrow q\underset{\dot{}}{\le }W\right)$$
25	24	notbid	$$⊢w=W\to \left(\neg q\underset{\dot{}}{\le }w\leftrightarrow \neg q\underset{\dot{}}{\le }W\right)$$
26		oveq2	$$⊢w=W\to x\underset{\dot{}}{\wedge }w=x\underset{\dot{}}{\wedge }W$$
27	26	oveq2d	$$⊢w=W\to q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)$$
28	27	eqeq1d	$$⊢w=W\to \left(q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\leftrightarrow q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)$$
29	25 28	anbi12d	$$⊢w=W\to \left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\leftrightarrow \left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\right)$$
30	21	fveq2d	$$⊢w=W\to \mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)=\mathrm{LSSum}\left(U\right)$$
31	30 12	syl6eqr	$$⊢w=W\to \mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)=\underset{\dot{}}{\oplus }$$
32		fveq2	$$⊢w=W\to \mathrm{DIsoC}\left(K\right)\left(w\right)=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
33	32 9	syl6eqr	$$⊢w=W\to \mathrm{DIsoC}\left(K\right)\left(w\right)=C$$
34	33	fveq1d	$$⊢w=W\to \mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)=C\left(q\right)$$
35	18 26	fveq12d	$$⊢w=W\to \mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)=D\left(x\underset{\dot{}}{\wedge }W\right)$$
36	31 34 35	oveq123d	$$⊢w=W\to \mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)$$
37	36	eqeq2d	$$⊢w=W\to \left(u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\leftrightarrow u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)$$
38	29 37	imbi12d	$$⊢w=W\to \left(\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\leftrightarrow \left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)$$
39	38	ralbidv	$$⊢w=W\to \left(\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\leftrightarrow \forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)$$
40	23 39	riotaeqbidv	$$⊢w=W\to \left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)=\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)$$
41	16 19 40	ifbieq12d	$$⊢w=W\to if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)=if\left(x\underset{\dot{}}{\le }W,D\left(x\right),\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)\right)$$
42	41	mpteq2dv	$$⊢w=W\to \left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)=\left(x\in B⟼if\left(x\underset{\dot{}}{\le }W,D\left(x\right),\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)\right)\right)$$
43		eqid	$$⊢\left(w\in H⟼\left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)\right)=\left(w\in H⟼\left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)\right)$$
44	42 43 1	mptfvmpt	$$⊢W\in H\to \left(w\in H⟼\left(x\in B⟼if\left(x\underset{\dot{}}{\le }w,\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }w\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=x\right)\to u=\mathrm{DIsoC}\left(K\right)\left(w\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(w\right)\right)\mathrm{DIsoB}\left(K\right)\left(w\right)\left(x\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\right)\right)\left(W\right)=\left(x\in B⟼if\left(x\underset{\dot{}}{\le }W,D\left(x\right),\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)\right)\right)$$
45	15 44	sylan9eq	$$⊢\left(K\in V\wedge W\in H\right)\to I=\left(x\in B⟼if\left(x\underset{\dot{}}{\le }W,D\left(x\right),\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=x\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)\right)\right)\right)\right)$$