Metamath Proof Explorer

Theorem thlbas

Description: Base set of the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015) (Proof shortened by AV, 11-Nov-2024)

Ref Expression
Hypotheses thlval.k ⊢ 𝐾 = ( toHL ‘ 𝑊 )
thlbas.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion thlbas 𝐶 = ( Base ‘ 𝐾 )

Proof

Step Hyp Ref Expression
1 thlval.k ⊢ 𝐾 = ( toHL ‘ 𝑊 )
2 thlbas.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3 2 fvexi ⊢ 𝐶 ∈ V
4 eqid ⊢ ( toInc ‘ 𝐶 ) = ( toInc ‘ 𝐶 )
5 4 ipobas ⊢ ( 𝐶 ∈ V → 𝐶 = ( Base ‘ ( toInc ‘ 𝐶 ) ) )
6 3 5 ax-mp ⊢ 𝐶 = ( Base ‘ ( toInc ‘ 𝐶 ) )
7 baseid ⊢ Base = Slot ( Base ‘ ndx )
8 basendxnocndx ⊢ ( Base ‘ ndx ) ≠ ( oc ‘ ndx )
9 7 8 setsnid ⊢ ( Base ‘ ( toInc ‘ 𝐶 ) ) = ( Base ‘ ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
10 6 9 eqtri ⊢ 𝐶 = ( Base ‘ ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
11 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
12 1 2 4 11 thlval ⊢ ( 𝑊 ∈ V → 𝐾 = ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
13 12 fveq2d ⊢ ( 𝑊 ∈ V → ( Base ‘ 𝐾 ) = ( Base ‘ ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) ) )
14 10 13 eqtr4id ⊢ ( 𝑊 ∈ V → 𝐶 = ( Base ‘ 𝐾 ) )
15 base0 ⊢ ∅ = ( Base ‘ ∅ )
16 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( ClSubSp ‘ 𝑊 ) = ∅ )
17 2 16 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐶 = ∅ )
18 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
19 1 18 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
20 19 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝐾 ) = ( Base ‘ ∅ ) )
21 15 17 20 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → 𝐶 = ( Base ‘ 𝐾 ) )
22 14 21 pm2.61i ⊢ 𝐶 = ( Base ‘ 𝐾 )