Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
dalemqrprot
Next ⟩
dalemyeb
Metamath Proof Explorer
Ascii
Unicode
Theorem
dalemqrprot
Description:
Lemma for
dath
. Frequently-used utility lemma.
(Contributed by
NM
, 13-Aug-2012)
Ref
Expression
Hypotheses
dalema.ph
⊢
φ
↔
K
∈
HL
∧
C
∈
Base
K
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
Y
∈
O
∧
Z
∈
O
∧
¬
C
≤
˙
P
∨
˙
Q
∧
¬
C
≤
˙
Q
∨
˙
R
∧
¬
C
≤
˙
R
∨
˙
P
∧
¬
C
≤
˙
S
∨
˙
T
∧
¬
C
≤
˙
T
∨
˙
U
∧
¬
C
≤
˙
U
∨
˙
S
∧
C
≤
˙
P
∨
˙
S
∧
C
≤
˙
Q
∨
˙
T
∧
C
≤
˙
R
∨
˙
U
dalemb.j
⊢
∨
˙
=
join
⁡
K
dalemb.a
⊢
A
=
Atoms
⁡
K
Assertion
dalemqrprot
⊢
φ
→
Q
∨
˙
R
∨
˙
P
=
P
∨
˙
Q
∨
˙
R
Proof
Step
Hyp
Ref
Expression
1
dalema.ph
⊢
φ
↔
K
∈
HL
∧
C
∈
Base
K
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
Y
∈
O
∧
Z
∈
O
∧
¬
C
≤
˙
P
∨
˙
Q
∧
¬
C
≤
˙
Q
∨
˙
R
∧
¬
C
≤
˙
R
∨
˙
P
∧
¬
C
≤
˙
S
∨
˙
T
∧
¬
C
≤
˙
T
∨
˙
U
∧
¬
C
≤
˙
U
∨
˙
S
∧
C
≤
˙
P
∨
˙
S
∧
C
≤
˙
Q
∨
˙
T
∧
C
≤
˙
R
∨
˙
U
2
dalemb.j
⊢
∨
˙
=
join
⁡
K
3
dalemb.a
⊢
A
=
Atoms
⁡
K
4
1
dalemkehl
⊢
φ
→
K
∈
HL
5
1
dalemqea
⊢
φ
→
Q
∈
A
6
1
dalemrea
⊢
φ
→
R
∈
A
7
1
dalempea
⊢
φ
→
P
∈
A
8
2
3
hlatjrot
⊢
K
∈
HL
∧
Q
∈
A
∧
R
∈
A
∧
P
∈
A
→
Q
∨
˙
R
∨
˙
P
=
P
∨
˙
Q
∨
˙
R
9
4
5
6
7
8
syl13anc
⊢
φ
→
Q
∨
˙
R
∨
˙
P
=
P
∨
˙
Q
∨
˙
R