Metamath Proof Explorer


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 pleid le = Slot ( le ‘ ndx )
6 10re 1 0 ∈ ℝ
7 1nn0 1 ∈ ℕ0
8 0nn0 0 ∈ ℕ0
9 1nn 1 ∈ ℕ
10 0lt1 0 < 1
11 7 8 9 10 declt 1 0 < 1 1
12 6 11 ltneii 1 0 ≠ 1 1
13 plendx ( le ‘ ndx ) = 1 0
14 ocndx ( oc ‘ ndx ) = 1 1
15 13 14 neeq12i ( ( le ‘ ndx ) ≠ ( oc ‘ ndx ) ↔ 1 0 ≠ 1 1 )
16 12 15 mpbir ( le ‘ ndx ) ≠ ( oc ‘ ndx )
17 5 16 setsnid ( le ‘ 𝐼 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
18 4 17 eqtri = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
19 eqid ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
20 1 2 3 19 thlval ( 𝑊 ∈ V → 𝐾 = ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) )
21 20 fveq2d ( 𝑊 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐼 sSet ⟨ ( oc ‘ ndx ) , ( ocv ‘ 𝑊 ) ⟩ ) ) )
22 18 21 eqtr4id ( 𝑊 ∈ V → = ( le ‘ 𝐾 ) )
23 5 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 ‘ 𝐾 )