Theorem dih1dimc

Description: Isomorphism H at an atom not under W . (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih1dimc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dih1dimc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dih1dimc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dih1dimc.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
	dih1dimc.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dih1dimc.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dih1dimc.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dih1dimc.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dih1dimc.f	$$⊢F=\left(\iota f\in T|f\left(P\right)=Q\right)$$
Assertion	dih1dimc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=N\left(\left\{⟨F,{\mathrm{I}\upharpoonright }_T⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dih1dimc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dih1dimc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		dih1dimc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dih1dimc.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
5		dih1dimc.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		dih1dimc.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
7		dih1dimc.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
8		dih1dimc.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
9		dih1dimc.f	$$⊢F=\left(\iota f\in T|f\left(P\right)=Q\right)$$
10		eqid	$$⊢\mathrm{DIsoC}\left(K\right)\left(W\right)=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
11	1 2 3 10 6	dihvalcqat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\mathrm{DIsoC}\left(K\right)\left(W\right)\left(Q\right)$$
12	1 2 3 4 5 10 7 8 9	diclspsn	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to \mathrm{DIsoC}\left(K\right)\left(W\right)\left(Q\right)=N\left(\left\{⟨F,{\mathrm{I}\upharpoonright }_T⟩\right\}\right)$$
13	11 12	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=N\left(\left\{⟨F,{\mathrm{I}\upharpoonright }_T⟩\right\}\right)$$