Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
lautm
Next ⟩
lauteq
Metamath Proof Explorer
Ascii
Unicode
Theorem
lautm
Description:
Meet property of a lattice automorphism.
(Contributed by
NM
, 19-May-2012)
Ref
Expression
Hypotheses
lautm.b
⊢
B
=
Base
K
lautm.m
⊢
∧
˙
=
meet
K
lautm.i
⊢
I
=
LAut
K
Assertion
lautm
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
=
F
X
∧
˙
F
Y
Proof
Step
Hyp
Ref
Expression
1
lautm.b
⊢
B
=
Base
K
2
lautm.m
⊢
∧
˙
=
meet
K
3
lautm.i
⊢
I
=
LAut
K
4
eqid
⊢
≤
K
=
≤
K
5
simpl
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
K
∈
Lat
6
simpr1
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
∈
I
7
5
6
jca
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
K
∈
Lat
∧
F
∈
I
8
1
2
latmcl
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
∈
B
9
8
3adant3r1
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
∈
B
10
1
3
lautcl
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∧
˙
Y
∈
B
→
F
X
∧
˙
Y
∈
B
11
7
9
10
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
∈
B
12
simpr2
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
X
∈
B
13
1
3
lautcl
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
→
F
X
∈
B
14
7
12
13
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∈
B
15
simpr3
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
Y
∈
B
16
1
3
lautcl
⊢
K
∈
Lat
∧
F
∈
I
∧
Y
∈
B
→
F
Y
∈
B
17
7
15
16
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
Y
∈
B
18
1
2
latmcl
⊢
K
∈
Lat
∧
F
X
∈
B
∧
F
Y
∈
B
→
F
X
∧
˙
F
Y
∈
B
19
5
14
17
18
syl3anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
F
Y
∈
B
20
1
4
2
latmle1
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
X
21
20
3adant3r1
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
X
22
1
4
3
lautle
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∧
˙
Y
∈
B
∧
X
∈
B
→
X
∧
˙
Y
≤
K
X
↔
F
X
∧
˙
Y
≤
K
F
X
23
7
9
12
22
syl12anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
X
↔
F
X
∧
˙
Y
≤
K
F
X
24
21
23
mpbid
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
≤
K
F
X
25
1
4
2
latmle2
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
Y
26
25
3adant3r1
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
Y
27
1
4
3
lautle
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∧
˙
Y
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
Y
↔
F
X
∧
˙
Y
≤
K
F
Y
28
7
9
15
27
syl12anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
X
∧
˙
Y
≤
K
Y
↔
F
X
∧
˙
Y
≤
K
F
Y
29
26
28
mpbid
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
≤
K
F
Y
30
1
4
2
latlem12
⊢
K
∈
Lat
∧
F
X
∧
˙
Y
∈
B
∧
F
X
∈
B
∧
F
Y
∈
B
→
F
X
∧
˙
Y
≤
K
F
X
∧
F
X
∧
˙
Y
≤
K
F
Y
↔
F
X
∧
˙
Y
≤
K
F
X
∧
˙
F
Y
31
5
11
14
17
30
syl13anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
≤
K
F
X
∧
F
X
∧
˙
Y
≤
K
F
Y
↔
F
X
∧
˙
Y
≤
K
F
X
∧
˙
F
Y
32
24
29
31
mpbi2and
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
≤
K
F
X
∧
˙
F
Y
33
1
3
laut1o
⊢
K
∈
Lat
∧
F
∈
I
→
F
:
B
⟶
1-1 onto
B
34
33
3ad2antr1
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
:
B
⟶
1-1 onto
B
35
f1ocnvfv2
⊢
F
:
B
⟶
1-1 onto
B
∧
F
X
∧
˙
F
Y
∈
B
→
F
F
-1
F
X
∧
˙
F
Y
=
F
X
∧
˙
F
Y
36
34
19
35
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
F
-1
F
X
∧
˙
F
Y
=
F
X
∧
˙
F
Y
37
1
4
2
latmle1
⊢
K
∈
Lat
∧
F
X
∈
B
∧
F
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
X
38
5
14
17
37
syl3anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
X
39
1
4
3
lautcnvle
⊢
K
∈
Lat
∧
F
∈
I
∧
F
X
∧
˙
F
Y
∈
B
∧
F
X
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
X
↔
F
-1
F
X
∧
˙
F
Y
≤
K
F
-1
F
X
40
7
19
14
39
syl12anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
X
↔
F
-1
F
X
∧
˙
F
Y
≤
K
F
-1
F
X
41
38
40
mpbid
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
F
-1
F
X
42
f1ocnvfv1
⊢
F
:
B
⟶
1-1 onto
B
∧
X
∈
B
→
F
-1
F
X
=
X
43
34
12
42
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
=
X
44
41
43
breqtrd
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
X
45
1
4
2
latmle2
⊢
K
∈
Lat
∧
F
X
∈
B
∧
F
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
Y
46
5
14
17
45
syl3anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
Y
47
1
4
3
lautcnvle
⊢
K
∈
Lat
∧
F
∈
I
∧
F
X
∧
˙
F
Y
∈
B
∧
F
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
Y
↔
F
-1
F
X
∧
˙
F
Y
≤
K
F
-1
F
Y
48
7
19
17
47
syl12anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
Y
↔
F
-1
F
X
∧
˙
F
Y
≤
K
F
-1
F
Y
49
46
48
mpbid
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
F
-1
F
Y
50
f1ocnvfv1
⊢
F
:
B
⟶
1-1 onto
B
∧
Y
∈
B
→
F
-1
F
Y
=
Y
51
34
15
50
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
Y
=
Y
52
49
51
breqtrd
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
Y
53
f1ocnvdm
⊢
F
:
B
⟶
1-1 onto
B
∧
F
X
∧
˙
F
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
∈
B
54
34
19
53
syl2anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
∈
B
55
1
4
2
latlem12
⊢
K
∈
Lat
∧
F
-1
F
X
∧
˙
F
Y
∈
B
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
F
-1
F
X
∧
˙
F
Y
≤
K
Y
↔
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
˙
Y
56
5
54
12
15
55
syl13anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
F
-1
F
X
∧
˙
F
Y
≤
K
Y
↔
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
˙
Y
57
44
52
56
mpbi2and
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
˙
Y
58
1
4
3
lautle
⊢
K
∈
Lat
∧
F
∈
I
∧
F
-1
F
X
∧
˙
F
Y
∈
B
∧
X
∧
˙
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
˙
Y
↔
F
F
-1
F
X
∧
˙
F
Y
≤
K
F
X
∧
˙
Y
59
7
54
9
58
syl12anc
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
-1
F
X
∧
˙
F
Y
≤
K
X
∧
˙
Y
↔
F
F
-1
F
X
∧
˙
F
Y
≤
K
F
X
∧
˙
Y
60
57
59
mpbid
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
F
-1
F
X
∧
˙
F
Y
≤
K
F
X
∧
˙
Y
61
36
60
eqbrtrrd
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
F
Y
≤
K
F
X
∧
˙
Y
62
1
4
5
11
19
32
61
latasymd
⊢
K
∈
Lat
∧
F
∈
I
∧
X
∈
B
∧
Y
∈
B
→
F
X
∧
˙
Y
=
F
X
∧
˙
F
Y