Theorem lhpset

Description: The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012)

	Ref	Expression
Hypotheses	lhpset.b	$$⊢B={\mathrm{Base}}_K$$
	lhpset.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	lhpset.c	$$⊢C={⋖}_K$$
	lhpset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpset	$$⊢K\in A\to H=\left\{w\in B|wC\underset{\dot{}}{1}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lhpset.b	$$⊢B={\mathrm{Base}}_K$$
2		lhpset.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
3		lhpset.c	$$⊢C={⋖}_K$$
4		lhpset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		elex	$$⊢K\in A\to K\in \mathrm{V}$$
6		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
7	6 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
8		eqidd	$$⊢k=K\to w=w$$
9		fveq2	$$⊢k=K\to {⋖}_k={⋖}_K$$
10	9 3	eqtr4di	$$⊢k=K\to {⋖}_k=C$$
11		fveq2	$$⊢k=K\to \mathrm{1.}\left(k\right)=\mathrm{1.}\left(K\right)$$
12	11 2	eqtr4di	$$⊢k=K\to \mathrm{1.}\left(k\right)=\underset{\dot{}}{1}$$
13	8 10 12	breq123d	$$⊢k=K\to \left(w{⋖}_k\mathrm{1.}\left(k\right)\leftrightarrow wC\underset{\dot{}}{1}\right)$$
14	7 13	rabeqbidv	$$⊢k=K\to \left\{w\in {\mathrm{Base}}_k|w{⋖}_k\mathrm{1.}\left(k\right)\right\}=\left\{w\in B|wC\underset{\dot{}}{1}\right\}$$
15		df-lhyp	$$⊢\mathrm{LHyp}=\left(k\in \mathrm{V}⟼\left\{w\in {\mathrm{Base}}_k|w{⋖}_k\mathrm{1.}\left(k\right)\right\}\right)$$
16	1	fvexi	$$⊢B\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{w\in B|wC\underset{\dot{}}{1}\right\}\in \mathrm{V}$$
18	14 15 17	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{LHyp}\left(K\right)=\left\{w\in B|wC\underset{\dot{}}{1}\right\}$$
19	4 18	syl5eq	$$⊢K\in \mathrm{V}\to H=\left\{w\in B|wC\underset{\dot{}}{1}\right\}$$
20	5 19	syl	$$⊢K\in A\to H=\left\{w\in B|wC\underset{\dot{}}{1}\right\}$$