thlle

Description: Ordering on 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 ‘ 𝑊 )
	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		pleid	⊢ le = Slot ( le ‘ ndx )
6		plendxnocndx	⊢ ( le ‘ ndx ) ≠ ( oc ‘ ndx )
7	5 6	setsnid	⊢ ( le ‘ 𝐼 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
8	4 7	eqtri	⊢ ≤ = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
9		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
10	1 2 3 9	thlval	⊢ ( 𝑊 ∈ V → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
11	10	fveq2d	⊢ ( 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) ) )
12	8 11	eqtr4id	⊢ ( 𝑊 ∈ V → ≤ = ( le ‘ 𝐾 ) )
13	5	str0	⊢ ∅ = ( le ‘ ∅ )
14	2	fvexi	⊢ 𝐶 ∈ V
15	3	ipolerval	⊢ ( 𝐶 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )
16	14 15	ax-mp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 )
17	4 16	eqtr4i	⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) }
18		opabn0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) )
19		vex	⊢ 𝑥 ∈ V
20		vex	⊢ 𝑦 ∈ V
21	19 20	prss	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐶 )
22		elfvex	⊢ ( 𝑥 ∈ ( ClSubSp ‘ 𝑊 ) → 𝑊 ∈ V )
23	22 2	eleq2s	⊢ ( 𝑥 ∈ 𝐶 → 𝑊 ∈ V )
24	23	ad2antrr	⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
25	21 24	sylanbr	⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
26	25	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) → 𝑊 ∈ V )
27	18 26	sylbi	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } ≠ ∅ → 𝑊 ∈ V )
28	27	necon1bi	⊢ ( ¬ 𝑊 ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐶 ∧ 𝑥 ⊆ 𝑦 ) } = ∅ )
29	17 28	eqtrid	⊢ ( ¬ 𝑊 ∈ V → ≤ = ∅ )
30		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
31	1 30	eqtrid	⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
32	31	fveq2d	⊢ ( ¬ 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ∅ ) )
33	13 29 32	3eqtr4a	⊢ ( ¬ 𝑊 ∈ V → ≤ = ( le ‘ 𝐾 ) )
34	12 33	pm2.61i	⊢ ≤ = ( le ‘ 𝐾 )

Metamath Proof Explorer

Theorem thlle

Proof