Metamath Proof Explorer

Theorem thlbasOLD

Description: Obsolete proof of thlbas as of 11-Nov-2024. Base set of the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses thlval.k ⊢ 𝐾 = ( toHL ‘ 𝑊 )
thlbas.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion thlbasOLD 𝐶 = ( 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 1re ⊢ 1 ∈ ℝ
9 1nn ⊢ 1 ∈ ℕ
10 1nn0 ⊢ 1 ∈ ℕ0
11 1lt10 ⊢ 1 < 1 0
12 9 10 10 11 declti ⊢ 1 < 1 1
13 8 12 ltneii ⊢ 1 ≠ 1 1
14 basendx ⊢ ( Base ‘ ndx ) = 1
15 ocndx ⊢ ( oc ‘ ndx ) = 1 1
16 14 15 neeq12i ⊢ ( ( Base ‘ ndx ) ≠ ( oc ‘ ndx ) ↔ 1 ≠ 1 1 )
17 13 16 mpbir ⊢ ( Base ‘ ndx ) ≠ ( oc ‘ ndx )
18 7 17 setsnid ⊢ ( Base ‘ ( toInc ‘ 𝐶 ) ) = ( Base ‘ ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
19 6 18 eqtri ⊢ 𝐶 = ( Base ‘ ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
20 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
21 1 2 4 20 thlval ⊢ ( 𝑊 ∈ V → 𝐾 = ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
22 21 fveq2d ⊢ ( 𝑊 ∈ V → ( Base ‘ 𝐾 ) = ( Base ‘ ( ( toInc ‘ 𝐶 ) sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) ) )
23 19 22 eqtr4id ⊢ ( 𝑊 ∈ V → 𝐶 = ( Base ‘ 𝐾 ) )
24 base0 ⊢ ∅ = ( Base ‘ ∅ )
25 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( ClSubSp ‘ 𝑊 ) = ∅ )
26 2 25 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐶 = ∅ )
27 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
28 1 27 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
29 28 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝐾 ) = ( Base ‘ ∅ ) )
30 24 26 29 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → 𝐶 = ( Base ‘ 𝐾 ) )
31 23 30 pm2.61i ⊢ 𝐶 = ( Base ‘ 𝐾 )