Theorem dihmeetlem14N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetlem14.b	$$⊢B={\mathrm{Base}}_K$$
	dihmeetlem14.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihmeetlem14.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihmeetlem14.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihmeetlem14.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihmeetlem14.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihmeetlem14.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihmeetlem14.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihmeetlem14.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
Assertion	dihmeetlem14N	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Y\in B\wedge p\in B\right)\wedge \left(\left(r\in A\wedge \neg r\underset{\dot{}}{\le }W\right)\wedge r\underset{\dot{}}{\le }Y\wedge \left(Y\underset{\dot{}}{\wedge }p\right)\underset{\dot{}}{\le }W\right)\right)\to I\left(Y\underset{\dot{}}{\wedge }p\right)\underset{\dot{}}{\oplus }\left(I\left(r\right)\cap I\left(p\right)\right)=I\left(Y\right)\cap I\left(p\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem14.b	$$⊢B={\mathrm{Base}}_K$$
2		dihmeetlem14.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihmeetlem14.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dihmeetlem14.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		dihmeetlem14.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
6		dihmeetlem14.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
7		dihmeetlem14.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
8		dihmeetlem14.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
9		dihmeetlem14.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
10	1 2 3 4 5 6 7 8 9	dihmeetlem12N	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Y\in B\wedge p\in B\right)\wedge \left(\left(r\in A\wedge \neg r\underset{\dot{}}{\le }W\right)\wedge r\underset{\dot{}}{\le }Y\wedge \left(Y\underset{\dot{}}{\wedge }p\right)\underset{\dot{}}{\le }W\right)\right)\to I\left(Y\underset{\dot{}}{\wedge }p\right)\underset{\dot{}}{\oplus }\left(I\left(r\right)\cap I\left(p\right)\right)=I\left(Y\right)\cap I\left(p\right)$$