Metamath Proof Explorer

Theorem psubclsetN

Description: The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses psubclset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
psubclset.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
psubclset.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion psubclsetN ( 𝐾 ∈ 𝐵 → 𝐶 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } )

Proof

Step Hyp Ref Expression
1 psubclset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 psubclset.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 psubclset.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
5 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
6 5 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
7 6 sseq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ↔ 𝑠 ⊆ 𝐴 ) )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ⊥𝑃 ‘ 𝑘 ) = ( ⊥𝑃 ‘ 𝐾 ) )
9 8 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( ⊥𝑃 ‘ 𝑘 ) = ⊥ )
10 9 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) = ( ⊥ ‘ 𝑠 ) )
11 9 10 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) )
12 11 eqeq1d ⊢ ( 𝑘 = 𝐾 → ( ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) )
13 7 12 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) ↔ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) ) )
14 13 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } )
15 df-psubclN ⊢ PSubCl = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) } )
16 1 fvexi ⊢ 𝐴 ∈ V
17 16 pwex ⊢ 𝒫 𝐴 ∈ V
18 velpw ⊢ ( 𝑠 ∈ 𝒫 𝐴 ↔ 𝑠 ⊆ 𝐴 )
19 18 anbi1i ⊢ ( ( 𝑠 ∈ 𝒫 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) ↔ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) )
20 19 abbii ⊢ { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) }
21 ssab2 ⊢ { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } ⊆ 𝒫 𝐴
22 20 21 eqsstrri ⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } ⊆ 𝒫 𝐴
23 17 22 ssexi ⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } ∈ V
24 14 15 23 fvmpt ⊢ ( 𝐾 ∈ V → ( PSubCl ‘ 𝐾 ) = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } )
25 3 24 syl5eq ⊢ ( 𝐾 ∈ V → 𝐶 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } )
26 4 25 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝐶 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = 𝑠 ) } )