Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
idlaut
Next ⟩
lautco
Metamath Proof Explorer
Ascii
Unicode
Theorem
idlaut
Description:
The identity function is a lattice automorphism.
(Contributed by
NM
, 18-May-2012)
Ref
Expression
Hypotheses
idlaut.b
⊢
B
=
Base
K
idlaut.i
⊢
I
=
LAut
⁡
K
Assertion
idlaut
⊢
K
∈
A
→
I
↾
B
∈
I
Proof
Step
Hyp
Ref
Expression
1
idlaut.b
⊢
B
=
Base
K
2
idlaut.i
⊢
I
=
LAut
⁡
K
3
f1oi
⊢
I
↾
B
:
B
⟶
1-1 onto
B
4
3
a1i
⊢
K
∈
A
→
I
↾
B
:
B
⟶
1-1 onto
B
5
fvresi
⊢
x
∈
B
→
I
↾
B
⁡
x
=
x
6
fvresi
⊢
y
∈
B
→
I
↾
B
⁡
y
=
y
7
5
6
breqan12d
⊢
x
∈
B
∧
y
∈
B
→
I
↾
B
⁡
x
≤
K
I
↾
B
⁡
y
↔
x
≤
K
y
8
7
bicomd
⊢
x
∈
B
∧
y
∈
B
→
x
≤
K
y
↔
I
↾
B
⁡
x
≤
K
I
↾
B
⁡
y
9
8
rgen2
⊢
∀
x
∈
B
∀
y
∈
B
x
≤
K
y
↔
I
↾
B
⁡
x
≤
K
I
↾
B
⁡
y
10
9
a1i
⊢
K
∈
A
→
∀
x
∈
B
∀
y
∈
B
x
≤
K
y
↔
I
↾
B
⁡
x
≤
K
I
↾
B
⁡
y
11
eqid
⊢
≤
K
=
≤
K
12
1
11
2
islaut
⊢
K
∈
A
→
I
↾
B
∈
I
↔
I
↾
B
:
B
⟶
1-1 onto
B
∧
∀
x
∈
B
∀
y
∈
B
x
≤
K
y
↔
I
↾
B
⁡
x
≤
K
I
↾
B
⁡
y
13
4
10
12
mpbir2and
⊢
K
∈
A
→
I
↾
B
∈
I