Theorem thlbas

Description: Base set of the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015)

	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		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	syl5eq	⊢ ( ¬ 𝑊 ∈ V → 𝐶 = ∅ )
27		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
28	1 27	syl5eq	⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
29	28	fveq2d	⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝐾 ) = ( Base ‘ ∅ ) )
30	24 26 29	3eqtr4a	⊢ ( ¬ 𝑊 ∈ V → 𝐶 = ( Base ‘ 𝐾 ) )
31	23 30	pm2.61i	⊢ 𝐶 = ( Base ‘ 𝐾 )