Theorem dihmeetlem7N

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

	Ref	Expression
Hypotheses	dihmeetlem7.b	$$⊢B={\mathrm{Base}}_K$$
	dihmeetlem7.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihmeetlem7.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihmeetlem7.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihmeetlem7.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	dihmeetlem7N	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }p\right)\underset{\dot{}}{\wedge }Y=X\underset{\dot{}}{\wedge }Y$$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem7.b	$$⊢B={\mathrm{Base}}_K$$
2		dihmeetlem7.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihmeetlem7.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihmeetlem7.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		dihmeetlem7.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		simprr	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \neg p\underset{\dot{}}{\le }Y$$
7		simpl1	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to K\in \mathrm{HL}$$
8		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
9	7 8	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to K\in \mathrm{AtLat}$$
10		simprl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to p\in A$$
11		simpl3	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to Y\in B$$
12		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
13	1 2 4 12 5	atnle	$$⊢\left(K\in \mathrm{AtLat}\wedge p\in A\wedge Y\in B\right)\to \left(\neg p\underset{\dot{}}{\le }Y\leftrightarrow p\underset{\dot{}}{\wedge }Y=\mathrm{0.}\left(K\right)\right)$$
14	9 10 11 13	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(\neg p\underset{\dot{}}{\le }Y\leftrightarrow p\underset{\dot{}}{\wedge }Y=\mathrm{0.}\left(K\right)\right)$$
15	6 14	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to p\underset{\dot{}}{\wedge }Y=\mathrm{0.}\left(K\right)$$
16	15	oveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\left(p\underset{\dot{}}{\wedge }Y\right)=\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\mathrm{0.}\left(K\right)$$
17	7	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to K\in \mathrm{Lat}$$
18		simpl2	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to X\in B$$
19	1 4	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\wedge }Y\in B$$
20	17 18 11 19	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to X\underset{\dot{}}{\wedge }Y\in B$$
21	1 2 4	latmle2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y$$
22	17 18 11 21	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y$$
23	1 2 3 4 5	atmod1i2	$$⊢\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge X\underset{\dot{}}{\wedge }Y\in B\wedge Y\in B\right)\wedge \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }Y\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\left(p\underset{\dot{}}{\wedge }Y\right)=\left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }p\right)\underset{\dot{}}{\wedge }Y$$
24	7 10 20 11 22 23	syl131anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\left(p\underset{\dot{}}{\wedge }Y\right)=\left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }p\right)\underset{\dot{}}{\wedge }Y$$
25		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
26	7 25	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to K\in \mathrm{OL}$$
27	1 3 12	olj01	$$⊢\left(K\in \mathrm{OL}\wedge X\underset{\dot{}}{\wedge }Y\in B\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\mathrm{0.}\left(K\right)=X\underset{\dot{}}{\wedge }Y$$
28	26 20 27	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\mathrm{0.}\left(K\right)=X\underset{\dot{}}{\wedge }Y$$
29	16 24 28	3eqtr3d	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\wedge \left(p\in A\wedge \neg p\underset{\dot{}}{\le }Y\right)\right)\to \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }p\right)\underset{\dot{}}{\wedge }Y=X\underset{\dot{}}{\wedge }Y$$