Theorem djhfval

Description: Subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

	Ref	Expression
Hypotheses	djhval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	djhval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	djhval.v	$$⊢V={\mathrm{Base}}_U$$
	djhval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	djhval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
Assertion	djhfval	$$⊢\left(K\in X\wedge W\in H\right)\to \underset{\dot{}}{\vee }=\left(x\in 𝒫V,y\in 𝒫V⟼\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		djhval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		djhval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		djhval.v	$$⊢V={\mathrm{Base}}_U$$
4		djhval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
5		djhval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
6	1	djhffval	$$⊢K\in X\to \mathrm{joinH}\left(K\right)=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)\right)$$
7	6	fveq1d	$$⊢K\in X\to \mathrm{joinH}\left(K\right)\left(W\right)=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)\right)\left(W\right)$$
8	5 7	syl5eq	$$⊢K\in X\to \underset{\dot{}}{\vee }=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)\right)\left(W\right)$$
9		2fveq3	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
10	2	fveq2i	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
11	3 10	eqtri	$$⊢V={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
12	9 11	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}=V$$
13	12	pweqd	$$⊢w=W\to 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}=𝒫V$$
14		fveq2	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
15	14 4	eqtr4di	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)=\underset{\dot{}}{\perp }$$
16	15	fveq1d	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)=\underset{\dot{}}{\perp }\left(x\right)$$
17	15	fveq1d	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)=\underset{\dot{}}{\perp }\left(y\right)$$
18	16 17	ineq12d	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)=\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)$$
19	15 18	fveq12d	$$⊢w=W\to \mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)\right)$$
20	13 13 19	mpoeq123dv	$$⊢w=W\to \left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)=\left(x\in 𝒫V,y\in 𝒫V⟼\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)\right)\right)$$
21		eqid	$$⊢\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)\right)=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)\right)$$
22	3	fvexi	$$⊢V\in \mathrm{V}$$
23	22	pwex	$$⊢𝒫V\in \mathrm{V}$$
24	23 23	mpoex	$$⊢\left(x\in 𝒫V,y\in 𝒫V⟼\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)\right)\right)\in \mathrm{V}$$
25	20 21 24	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)},y\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{ocH}\left(K\right)\left(w\right)\left(\mathrm{ocH}\left(K\right)\left(w\right)\left(x\right)\cap \mathrm{ocH}\left(K\right)\left(w\right)\left(y\right)\right)\right)\right)\left(W\right)=\left(x\in 𝒫V,y\in 𝒫V⟼\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)\right)\right)$$
26	8 25	sylan9eq	$$⊢\left(K\in X\wedge W\in H\right)\to \underset{\dot{}}{\vee }=\left(x\in 𝒫V,y\in 𝒫V⟼\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\cap \underset{\dot{}}{\perp }\left(y\right)\right)\right)$$