lpolsetN

Description: The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lpolset.v	$⊢ V = {Base}_{W}$
	lpolset.s	$⊢ S = LSubSp (W)$
	lpolset.z	$⊢ \underset{˙}{0} = 0_{W}$
	lpolset.a	$⊢ A = LSAtoms (W)$
	lpolset.h	$⊢ H = LSHyp (W)$
	lpolset.p	$⊢ P = LPol (W)$
Assertion	lpolsetN	$⊢ W \in X \to P = \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\}$

Proof

Step	Hyp	Ref	Expression
1		lpolset.v	$⊢ V = {Base}_{W}$
2		lpolset.s	$⊢ S = LSubSp (W)$
3		lpolset.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lpolset.a	$⊢ A = LSAtoms (W)$
5		lpolset.h	$⊢ H = LSHyp (W)$
6		lpolset.p	$⊢ P = LPol (W)$
7		elex	$⊢ W \in X \to W \in V$
8		fveq2	$⊢ w = W \to LSubSp (w) = LSubSp (W)$
9	8 2	eqtr4di	$⊢ w = W \to LSubSp (w) = S$
10		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
11	10 1	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
12	11	pweqd	$⊢ w = W \to 𝒫 {Base}_{w} = 𝒫 V$
13	9 12	oveq12d	$⊢ w = W \to {LSubSp (w)}^{𝒫 {Base}_{w}} = S^{𝒫 V}$
14	11	fveq2d	$⊢ w = W \to o ({Base}_{w}) = o (V)$
15		fveq2	$⊢ w = W \to 0_{w} = 0_{W}$
16	15 3	eqtr4di	$⊢ w = W \to 0_{w} = \underset{˙}{0}$
17	16	sneqd	$⊢ w = W \to \{0_{w}\} = \{\underset{˙}{0}\}$
18	14 17	eqeq12d	$⊢ w = W \to (o ({Base}_{w}) = \{0_{w}\} \leftrightarrow o (V) = \{\underset{˙}{0}\})$
19	11	sseq2d	$⊢ w = W \to (x \subseteq {Base}_{w} \leftrightarrow x \subseteq V)$
20	11	sseq2d	$⊢ w = W \to (y \subseteq {Base}_{w} \leftrightarrow y \subseteq V)$
21	19 20	3anbi12d	$⊢ w = W \to ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \leftrightarrow (x \subseteq V \land y \subseteq V \land x \subseteq y))$
22	21	imbi1d	$⊢ w = W \to (((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \leftrightarrow ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)))$
23	22	2albidv	$⊢ w = W \to (\forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \leftrightarrow \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)))$
24		fveq2	$⊢ w = W \to LSAtoms (w) = LSAtoms (W)$
25	24 4	eqtr4di	$⊢ w = W \to LSAtoms (w) = A$
26		fveq2	$⊢ w = W \to LSHyp (w) = LSHyp (W)$
27	26 5	eqtr4di	$⊢ w = W \to LSHyp (w) = H$
28	27	eleq2d	$⊢ w = W \to (o (x) \in LSHyp (w) \leftrightarrow o (x) \in H)$
29	28	anbi1d	$⊢ w = W \to ((o (x) \in LSHyp (w) \land o (o (x)) = x) \leftrightarrow (o (x) \in H \land o (o (x)) = x))$
30	25 29	raleqbidv	$⊢ w = W \to (\forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x) \leftrightarrow \forall x \in A (o (x) \in H \land o (o (x)) = x))$
31	18 23 30	3anbi123d	$⊢ w = W \to ((o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x)) \leftrightarrow (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x)))$
32	13 31	rabeqbidv	$⊢ w = W \to \{o \in ({LSubSp (w)}^{𝒫 {Base}_{w}}) \| (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))\} = \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\}$
33		df-lpolN	$⊢ LPol = (w \in V ⟼ \{o \in ({LSubSp (w)}^{𝒫 {Base}_{w}}) \| (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))\})$
34		ovex	$⊢ S^{𝒫 V} \in V$
35	34	rabex	$⊢ \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\} \in V$
36	32 33 35	fvmpt	$⊢ W \in V \to LPol (W) = \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\}$
37	6 36	syl5eq	$⊢ W \in V \to P = \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\}$
38	7 37	syl	$⊢ W \in X \to P = \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\}$

Metamath Proof Explorer

Theorem lpolsetN

Proof