Theorem thlle

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

	Ref	Expression
Hypotheses	thlval.k	⊢ 𝐾 = ( toHL ‘ 𝑊 )
	thlbas.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
	thlle.i	⊢ 𝐼 = ( toInc ‘ 𝐶 )
	thlle.l	⊢ ≤ = ( le ‘ 𝐼 )
Assertion	thlle	⊢ ≤ = ( le ‘ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		thlval.k	⊢ 𝐾 = ( toHL ‘ 𝑊 )
2		thlbas.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		thlle.i	⊢ 𝐼 = ( toInc ‘ 𝐶 )
4		thlle.l	⊢ ≤ = ( le ‘ 𝐼 )
5		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
6	1 2 3 5	thlval	⊢ ( 𝑊 ∈ V → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
7	6	fveq2d	⊢ ( 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) ) )
8		pleid	⊢ le = Slot ( le ‘ ndx )
9		10re	⊢ ; 1 0 ∈ ℝ
10		1nn0	⊢ 1 ∈ ℕ0
11		0nn0	⊢ 0 ∈ ℕ0
12		1nn	⊢ 1 ∈ ℕ
13		0lt1	⊢ 0 < 1
14	10 11 12 13	declt	⊢ ; 1 0 < ; 1 1
15	9 14	ltneii	⊢ ; 1 0 ≠ ; 1 1
16		plendx	⊢ ( le ‘ ndx ) = ; 1 0
17		ocndx	⊢ ( oc ‘ ndx ) = ; 1 1
18	16 17	neeq12i	⊢ ( ( le ‘ ndx ) ≠ ( oc ‘ ndx ) ↔ ; 1 0 ≠ ; 1 1 )
19	15 18	mpbir	⊢ ( le ‘ ndx ) ≠ ( oc ‘ ndx )
20	8 19	setsnid	⊢ ( le ‘ 𝐼 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
21	4 20	eqtri	⊢ ≤ = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
22	7 21	syl6reqr	⊢ ( 𝑊 ∈ V → ≤ = ( le ‘ 𝐾 ) )
23	8	str0	⊢ ∅ = ( le ‘ ∅ )
24	2	fvexi	⊢ 𝐶 ∈ V
25	3	ipolerval	⊢ ( 𝐶 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )
26	24 25	ax-mp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 )
27	4 26	eqtr4i	⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) }
28		opabn0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) )
29		vex	⊢ 𝑥 ∈ V
30		vex	⊢ 𝑦 ∈ V
31	29 30	prss	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐶 )
32		elfvex	⊢ ( 𝑥 ∈ ( ClSubSp ‘ 𝑊 ) → 𝑊 ∈ V )
33	32 2	eleq2s	⊢ ( 𝑥 ∈ 𝐶 → 𝑊 ∈ V )
34	33	ad2antrr	⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
35	31 34	sylanbr	⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
36	35	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
37	28 36	sylbi	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } ≠ ∅ → 𝑊 ∈ V )
38	37	necon1bi	⊢ ( ¬ 𝑊 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ∅ )
39	27 38	syl5eq	⊢ ( ¬ 𝑊 ∈ V → ≤ = ∅ )
40		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
41	1 40	syl5eq	⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
42	41	fveq2d	⊢ ( ¬ 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ∅ ) )
43	23 39 42	3eqtr4a	⊢ ( ¬ 𝑊 ∈ V → ≤ = ( le ‘ 𝐾 ) )
44	22 43	pm2.61i	⊢ ≤ = ( le ‘ 𝐾 )