Metamath Proof Explorer

Theorem 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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lpolset.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lpolset.z ⊢ 0 = ( 0g ‘ 𝑊 )
lpolset.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lpolset.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lpolset.p ⊢ 𝑃 = ( LPol ‘ 𝑊 )
Assertion lpolsetN ( 𝑊 ∈ 𝑋 → 𝑃 = { 𝑜 ∈ ( 𝑆 ↑m 𝒫 𝑉 ) ∣ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )

Proof

Step Hyp Ref Expression
1 lpolset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lpolset.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lpolset.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 lpolset.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lpolset.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6 lpolset.p ⊢ 𝑃 = ( LPol ‘ 𝑊 )
7 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
9 8 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝑆 )
10 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
11 10 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
12 11 pweqd ⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
13 9 12 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) = ( 𝑆 ↑m 𝒫 𝑉 ) )
14 11 fveq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = ( 𝑜 ‘ 𝑉 ) )
15 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝑊 ) )
16 15 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = 0 )
17 16 sneqd ⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ 𝑤 ) } = { 0 } )
18 14 17 eqeq12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ↔ ( 𝑜 ‘ 𝑉 ) = { 0 } ) )
19 11 sseq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ↔ 𝑥 ⊆ 𝑉 ) )
20 11 sseq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑦 ⊆ ( Base ‘ 𝑤 ) ↔ 𝑦 ⊆ 𝑉 ) )
21 19 20 3anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) ↔ ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) ) )
22 21 imbi1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ↔ ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ) )
23 22 2albidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ) )
24 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSAtoms ‘ 𝑤 ) = ( LSAtoms ‘ 𝑊 ) )
25 24 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSAtoms ‘ 𝑤 ) = 𝐴 )
26 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSHyp ‘ 𝑤 ) = ( LSHyp ‘ 𝑊 ) )
27 26 5 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSHyp ‘ 𝑤 ) = 𝐻 )
28 27 eleq2d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ↔ ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ) )
29 28 anbi1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ↔ ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) )
30 25 29 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) )
31 18 23 30 3anbi123d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) ↔ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) ) )
32 13 31 rabeqbidv ⊢ ( 𝑤 = 𝑊 → { 𝑜 ∈ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) ∣ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } = { 𝑜 ∈ ( 𝑆 ↑m 𝒫 𝑉 ) ∣ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )
33 df-lpolN ⊢ LPol = ( 𝑤 ∈ V ↦ { 𝑜 ∈ ( ( LSubSp ‘ 𝑤 ) ↑m 𝒫 ( Base ‘ 𝑤 ) ) ∣ ( ( 𝑜 ‘ ( Base ‘ 𝑤 ) ) = { ( 0g ‘ 𝑤 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑦 ⊆ ( Base ‘ 𝑤 ) ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑤 ) ( ( 𝑜 ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑤 ) ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )
34 ovex ⊢ ( 𝑆 ↑m 𝒫 𝑉 ) ∈ V
35 34 rabex ⊢ { 𝑜 ∈ ( 𝑆 ↑m 𝒫 𝑉 ) ∣ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } ∈ V
36 32 33 35 fvmpt ⊢ ( 𝑊 ∈ V → ( LPol ‘ 𝑊 ) = { 𝑜 ∈ ( 𝑆 ↑m 𝒫 𝑉 ) ∣ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )
37 6 36 syl5eq ⊢ ( 𝑊 ∈ V → 𝑃 = { 𝑜 ∈ ( 𝑆 ↑m 𝒫 𝑉 ) ∣ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )
38 7 37 syl ⊢ ( 𝑊 ∈ 𝑋 → 𝑃 = { 𝑜 ∈ ( 𝑆 ↑m 𝒫 𝑉 ) ∣ ( ( 𝑜 ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑜 ‘ 𝑦 ) ⊆ ( 𝑜 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑜 ‘ 𝑥 ) ∈ 𝐻 ∧ ( 𝑜 ‘ ( 𝑜 ‘ 𝑥 ) ) = 𝑥 ) ) } )