Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
States on a Hilbert lattice and Godowski's equation
States on a Hilbert lattice
stlesi
Next ⟩
stji1i
Metamath Proof Explorer
Ascii
Unicode
Theorem
stlesi
Description:
Ordering law for states.
(Contributed by
NM
, 24-Oct-1999)
(New usage is discouraged.)
Ref
Expression
Hypotheses
stle.1
⊢
A
∈
C
ℋ
stle.2
⊢
B
∈
C
ℋ
Assertion
stlesi
⊢
S
∈
States
→
A
⊆
B
→
S
⁡
A
=
1
→
S
⁡
B
=
1
Proof
Step
Hyp
Ref
Expression
1
stle.1
⊢
A
∈
C
ℋ
2
stle.2
⊢
B
∈
C
ℋ
3
stle1
⊢
S
∈
States
→
B
∈
C
ℋ
→
S
⁡
B
≤
1
4
2
3
mpi
⊢
S
∈
States
→
S
⁡
B
≤
1
5
4
adantr
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
S
⁡
B
≤
1
6
1
2
stlei
⊢
S
∈
States
→
A
⊆
B
→
S
⁡
A
≤
S
⁡
B
7
6
imp
⊢
S
∈
States
∧
A
⊆
B
→
S
⁡
A
≤
S
⁡
B
8
7
adantrr
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
S
⁡
A
≤
S
⁡
B
9
breq1
⊢
S
⁡
A
=
1
→
S
⁡
A
≤
S
⁡
B
↔
1
≤
S
⁡
B
10
9
ad2antll
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
S
⁡
A
≤
S
⁡
B
↔
1
≤
S
⁡
B
11
8
10
mpbid
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
1
≤
S
⁡
B
12
stcl
⊢
S
∈
States
→
B
∈
C
ℋ
→
S
⁡
B
∈
ℝ
13
2
12
mpi
⊢
S
∈
States
→
S
⁡
B
∈
ℝ
14
1re
⊢
1
∈
ℝ
15
13
14
jctir
⊢
S
∈
States
→
S
⁡
B
∈
ℝ
∧
1
∈
ℝ
16
15
adantr
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
S
⁡
B
∈
ℝ
∧
1
∈
ℝ
17
letri3
⊢
S
⁡
B
∈
ℝ
∧
1
∈
ℝ
→
S
⁡
B
=
1
↔
S
⁡
B
≤
1
∧
1
≤
S
⁡
B
18
16
17
syl
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
S
⁡
B
=
1
↔
S
⁡
B
≤
1
∧
1
≤
S
⁡
B
19
5
11
18
mpbir2and
⊢
S
∈
States
∧
A
⊆
B
∧
S
⁡
A
=
1
→
S
⁡
B
=
1
20
19
exp32
⊢
S
∈
States
→
A
⊆
B
→
S
⁡
A
=
1
→
S
⁡
B
=
1