Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
padd02
Next ⟩
paddcom
Metamath Proof Explorer
Ascii
Unicode
Theorem
padd02
Description:
Projective subspace sum with an empty set.
(Contributed by
NM
, 11-Jan-2012)
Ref
Expression
Hypotheses
padd0.a
⊢
A
=
Atoms
⁡
K
padd0.p
⊢
+
˙
=
+
𝑃
⁡
K
Assertion
padd02
⊢
K
∈
B
∧
X
⊆
A
→
∅
+
˙
X
=
X
Proof
Step
Hyp
Ref
Expression
1
padd0.a
⊢
A
=
Atoms
⁡
K
2
padd0.p
⊢
+
˙
=
+
𝑃
⁡
K
3
simpl
⊢
K
∈
B
∧
X
⊆
A
→
K
∈
B
4
0ss
⊢
∅
⊆
A
5
4
a1i
⊢
K
∈
B
∧
X
⊆
A
→
∅
⊆
A
6
simpr
⊢
K
∈
B
∧
X
⊆
A
→
X
⊆
A
7
3
5
6
3jca
⊢
K
∈
B
∧
X
⊆
A
→
K
∈
B
∧
∅
⊆
A
∧
X
⊆
A
8
neirr
⊢
¬
∅
≠
∅
9
8
intnanr
⊢
¬
∅
≠
∅
∧
X
≠
∅
10
1
2
paddval0
⊢
K
∈
B
∧
∅
⊆
A
∧
X
⊆
A
∧
¬
∅
≠
∅
∧
X
≠
∅
→
∅
+
˙
X
=
∅
∪
X
11
7
9
10
sylancl
⊢
K
∈
B
∧
X
⊆
A
→
∅
+
˙
X
=
∅
∪
X
12
uncom
⊢
∅
∪
X
=
X
∪
∅
13
un0
⊢
X
∪
∅
=
X
14
12
13
eqtri
⊢
∅
∪
X
=
X
15
11
14
eqtrdi
⊢
K
∈
B
∧
X
⊆
A
→
∅
+
˙
X
=
X