Theorem dihval

Description: Value of isomorphism H for a lattice K . Definition of isomorphism map in Crawley p. 122 line 3. (Contributed by NM, 3-Feb-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	dihval	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\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)$$

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 7 8 9 10 11 12	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)$$
14	13	fveq1d	$$⊢\left(K\in V\wedge W\in H\right)\to I\left(X\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)\left(X\right)$$
15		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }W\leftrightarrow X\underset{\dot{}}{\le }W\right)$$
16		fveq2	$$⊢x=X\to D\left(x\right)=D\left(X\right)$$
17		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }W=X\underset{\dot{}}{\wedge }W$$
18	17	oveq2d	$$⊢x=X\to q\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }W\right)=q\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)$$
19		id	$$⊢x=X\to x=X$$
20	18 19	eqeq12d	$$⊢x=X\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)$$
21	20	anbi2d	$$⊢x=X\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)$$
22		fvoveq1	$$⊢x=X\to D\left(x\underset{\dot{}}{\wedge }W\right)=D\left(X\underset{\dot{}}{\wedge }W\right)$$
23	22	oveq2d	$$⊢x=X\to C\left(q\right)\underset{\dot{}}{\oplus }D\left(x\underset{\dot{}}{\wedge }W\right)=C\left(q\right)\underset{\dot{}}{\oplus }D\left(X\underset{\dot{}}{\wedge }W\right)$$
24	23	eqeq2d	$$⊢x=X\to \left(u=C\left(q\right)\underset{\dot{}}{\oplus }D\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)$$
25	21 24	imbi12d	$$⊢x=X\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=C\left(q\right)\underset{\dot{}}{\oplus }D\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)$$
26	25	ralbidv	$$⊢x=X\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=C\left(q\right)\underset{\dot{}}{\oplus }D\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)$$
27	26	riotabidv	$$⊢x=X\to \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)=\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)$$
28	15 16 27	ifbieq12d	$$⊢x=X\to 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)=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)$$
29		eqid	$$⊢\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)=\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)$$
30		fvex	$$⊢D\left(X\right)\in \mathrm{V}$$
31		riotaex	$$⊢\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)\in \mathrm{V}$$
32	30 31	ifex	$$⊢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)\in \mathrm{V}$$
33	28 29 32	fvmpt	$$⊢X\in B\to \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)\left(X\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)$$
34	14 33	sylan9eq	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\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)$$