Theorem hlateq

Description: The equality of two Hilbert lattice elements is determined by the atoms under them. ( chrelat4i analog.) (Contributed by NM, 24-May-2012)

	Ref	Expression
Hypotheses	hlatle.b	$$⊢B={\mathrm{Base}}_K$$
	hlatle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlatle.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlateq	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(\forall p\in A\left(p\underset{\dot{}}{\le }X\leftrightarrow p\underset{\dot{}}{\le }Y\right)\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlatle.b	$$⊢B={\mathrm{Base}}_K$$
2		hlatle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		hlatle.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		ralbiim	$$⊢\forall p\in A\left(p\underset{\dot{}}{\le }X\leftrightarrow p\underset{\dot{}}{\le }Y\right)\leftrightarrow \left(\forall p\in A\left(p\underset{\dot{}}{\le }X\to p\underset{\dot{}}{\le }Y\right)\wedge \forall p\in A\left(p\underset{\dot{}}{\le }Y\to p\underset{\dot{}}{\le }X\right)\right)$$
5	1 2 3	hlatle	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \forall p\in A\left(p\underset{\dot{}}{\le }X\to p\underset{\dot{}}{\le }Y\right)\right)$$
6	1 2 3	hlatle	$$⊢\left(K\in \mathrm{HL}\wedge Y\in B\wedge X\in B\right)\to \left(Y\underset{\dot{}}{\le }X\leftrightarrow \forall p\in A\left(p\underset{\dot{}}{\le }Y\to p\underset{\dot{}}{\le }X\right)\right)$$
7	6	3com23	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(Y\underset{\dot{}}{\le }X\leftrightarrow \forall p\in A\left(p\underset{\dot{}}{\le }Y\to p\underset{\dot{}}{\le }X\right)\right)$$
8	5 7	anbi12d	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\leftrightarrow \left(\forall p\in A\left(p\underset{\dot{}}{\le }X\to p\underset{\dot{}}{\le }Y\right)\wedge \forall p\in A\left(p\underset{\dot{}}{\le }Y\to p\underset{\dot{}}{\le }X\right)\right)\right)$$
9	4 8	bitr4id	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(\forall p\in A\left(p\underset{\dot{}}{\le }X\leftrightarrow p\underset{\dot{}}{\le }Y\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\right)$$
10		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
11	1 2	latasymb	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\leftrightarrow X=Y\right)$$
12	10 11	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\leftrightarrow X=Y\right)$$
13	9 12	bitrd	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(\forall p\in A\left(p\underset{\dot{}}{\le }X\leftrightarrow p\underset{\dot{}}{\le }Y\right)\leftrightarrow X=Y\right)$$