Database
BASIC TOPOLOGY
Metric subcomplex vector spaces
Subcomplex pre-Hilbert spaces
cphsubrglem
Next ⟩
cphreccllem
Metamath Proof Explorer
Ascii
Unicode
Theorem
cphsubrglem
Description:
Lemma for
cphsubrg
.
(Contributed by
Mario Carneiro
, 9-Oct-2015)
Ref
Expression
Hypotheses
cphsubrglem.k
⊢
K
=
Base
F
cphsubrglem.1
⊢
φ
→
F
=
ℂ
fld
↾
𝑠
A
cphsubrglem.2
⊢
φ
→
F
∈
DivRing
Assertion
cphsubrglem
⊢
φ
→
F
=
ℂ
fld
↾
𝑠
K
∧
K
=
A
∩
ℂ
∧
K
∈
SubRing
ℂ
fld
Proof
Step
Hyp
Ref
Expression
1
cphsubrglem.k
⊢
K
=
Base
F
2
cphsubrglem.1
⊢
φ
→
F
=
ℂ
fld
↾
𝑠
A
3
cphsubrglem.2
⊢
φ
→
F
∈
DivRing
4
2
fveq2d
⊢
φ
→
Base
F
=
Base
ℂ
fld
↾
𝑠
A
5
drngring
⊢
F
∈
DivRing
→
F
∈
Ring
6
3
5
syl
⊢
φ
→
F
∈
Ring
7
2
6
eqeltrrd
⊢
φ
→
ℂ
fld
↾
𝑠
A
∈
Ring
8
eqid
⊢
Base
ℂ
fld
↾
𝑠
A
=
Base
ℂ
fld
↾
𝑠
A
9
eqid
⊢
0
ℂ
fld
↾
𝑠
A
=
0
ℂ
fld
↾
𝑠
A
10
8
9
ring0cl
⊢
ℂ
fld
↾
𝑠
A
∈
Ring
→
0
ℂ
fld
↾
𝑠
A
∈
Base
ℂ
fld
↾
𝑠
A
11
reldmress
⊢
Rel
dom
↾
𝑠
12
eqid
⊢
ℂ
fld
↾
𝑠
A
=
ℂ
fld
↾
𝑠
A
13
11
12
8
elbasov
⊢
0
ℂ
fld
↾
𝑠
A
∈
Base
ℂ
fld
↾
𝑠
A
→
ℂ
fld
∈
V
∧
A
∈
V
14
7
10
13
3syl
⊢
φ
→
ℂ
fld
∈
V
∧
A
∈
V
15
14
simprd
⊢
φ
→
A
∈
V
16
cnfldbas
⊢
ℂ
=
Base
ℂ
fld
17
12
16
ressbas
⊢
A
∈
V
→
A
∩
ℂ
=
Base
ℂ
fld
↾
𝑠
A
18
15
17
syl
⊢
φ
→
A
∩
ℂ
=
Base
ℂ
fld
↾
𝑠
A
19
4
18
eqtr4d
⊢
φ
→
Base
F
=
A
∩
ℂ
20
1
19
eqtrid
⊢
φ
→
K
=
A
∩
ℂ
21
20
oveq2d
⊢
φ
→
ℂ
fld
↾
𝑠
K
=
ℂ
fld
↾
𝑠
A
∩
ℂ
22
16
ressinbas
⊢
A
∈
V
→
ℂ
fld
↾
𝑠
A
=
ℂ
fld
↾
𝑠
A
∩
ℂ
23
15
22
syl
⊢
φ
→
ℂ
fld
↾
𝑠
A
=
ℂ
fld
↾
𝑠
A
∩
ℂ
24
21
23
eqtr4d
⊢
φ
→
ℂ
fld
↾
𝑠
K
=
ℂ
fld
↾
𝑠
A
25
2
24
eqtr4d
⊢
φ
→
F
=
ℂ
fld
↾
𝑠
K
26
25
6
eqeltrrd
⊢
φ
→
ℂ
fld
↾
𝑠
K
∈
Ring
27
cnring
⊢
ℂ
fld
∈
Ring
28
26
27
jctil
⊢
φ
→
ℂ
fld
∈
Ring
∧
ℂ
fld
↾
𝑠
K
∈
Ring
29
12
16
ressbasss
⊢
Base
ℂ
fld
↾
𝑠
A
⊆
ℂ
30
4
29
eqsstrdi
⊢
φ
→
Base
F
⊆
ℂ
31
1
30
eqsstrid
⊢
φ
→
K
⊆
ℂ
32
eqid
⊢
0
F
=
0
F
33
eqid
⊢
1
F
=
1
F
34
32
33
drngunz
⊢
F
∈
DivRing
→
1
F
≠
0
F
35
3
34
syl
⊢
φ
→
1
F
≠
0
F
36
25
fveq2d
⊢
φ
→
0
F
=
0
ℂ
fld
↾
𝑠
K
37
ringgrp
⊢
ℂ
fld
∈
Ring
→
ℂ
fld
∈
Grp
38
27
37
mp1i
⊢
φ
→
ℂ
fld
∈
Grp
39
ringgrp
⊢
ℂ
fld
↾
𝑠
K
∈
Ring
→
ℂ
fld
↾
𝑠
K
∈
Grp
40
26
39
syl
⊢
φ
→
ℂ
fld
↾
𝑠
K
∈
Grp
41
16
issubg
⊢
K
∈
SubGrp
ℂ
fld
↔
ℂ
fld
∈
Grp
∧
K
⊆
ℂ
∧
ℂ
fld
↾
𝑠
K
∈
Grp
42
38
31
40
41
syl3anbrc
⊢
φ
→
K
∈
SubGrp
ℂ
fld
43
eqid
⊢
ℂ
fld
↾
𝑠
K
=
ℂ
fld
↾
𝑠
K
44
cnfld0
⊢
0
=
0
ℂ
fld
45
43
44
subg0
⊢
K
∈
SubGrp
ℂ
fld
→
0
=
0
ℂ
fld
↾
𝑠
K
46
42
45
syl
⊢
φ
→
0
=
0
ℂ
fld
↾
𝑠
K
47
36
46
eqtr4d
⊢
φ
→
0
F
=
0
48
35
47
neeqtrd
⊢
φ
→
1
F
≠
0
49
48
neneqd
⊢
φ
→
¬
1
F
=
0
50
1
33
ringidcl
⊢
F
∈
Ring
→
1
F
∈
K
51
6
50
syl
⊢
φ
→
1
F
∈
K
52
31
51
sseldd
⊢
φ
→
1
F
∈
ℂ
53
52
sqvald
⊢
φ
→
1
F
2
=
1
F
1
F
54
25
fveq2d
⊢
φ
→
1
F
=
1
ℂ
fld
↾
𝑠
K
55
54
oveq1d
⊢
φ
→
1
F
1
F
=
1
ℂ
fld
↾
𝑠
K
1
F
56
25
fveq2d
⊢
φ
→
Base
F
=
Base
ℂ
fld
↾
𝑠
K
57
1
56
eqtrid
⊢
φ
→
K
=
Base
ℂ
fld
↾
𝑠
K
58
51
57
eleqtrd
⊢
φ
→
1
F
∈
Base
ℂ
fld
↾
𝑠
K
59
eqid
⊢
Base
ℂ
fld
↾
𝑠
K
=
Base
ℂ
fld
↾
𝑠
K
60
1
fvexi
⊢
K
∈
V
61
cnfldmul
⊢
×
=
⋅
ℂ
fld
62
43
61
ressmulr
⊢
K
∈
V
→
×
=
⋅
ℂ
fld
↾
𝑠
K
63
60
62
ax-mp
⊢
×
=
⋅
ℂ
fld
↾
𝑠
K
64
eqid
⊢
1
ℂ
fld
↾
𝑠
K
=
1
ℂ
fld
↾
𝑠
K
65
59
63
64
ringlidm
⊢
ℂ
fld
↾
𝑠
K
∈
Ring
∧
1
F
∈
Base
ℂ
fld
↾
𝑠
K
→
1
ℂ
fld
↾
𝑠
K
1
F
=
1
F
66
26
58
65
syl2anc
⊢
φ
→
1
ℂ
fld
↾
𝑠
K
1
F
=
1
F
67
53
55
66
3eqtrd
⊢
φ
→
1
F
2
=
1
F
68
sq01
⊢
1
F
∈
ℂ
→
1
F
2
=
1
F
↔
1
F
=
0
∨
1
F
=
1
69
52
68
syl
⊢
φ
→
1
F
2
=
1
F
↔
1
F
=
0
∨
1
F
=
1
70
67
69
mpbid
⊢
φ
→
1
F
=
0
∨
1
F
=
1
71
70
ord
⊢
φ
→
¬
1
F
=
0
→
1
F
=
1
72
49
71
mpd
⊢
φ
→
1
F
=
1
73
72
51
eqeltrrd
⊢
φ
→
1
∈
K
74
31
73
jca
⊢
φ
→
K
⊆
ℂ
∧
1
∈
K
75
cnfld1
⊢
1
=
1
ℂ
fld
76
16
75
issubrg
⊢
K
∈
SubRing
ℂ
fld
↔
ℂ
fld
∈
Ring
∧
ℂ
fld
↾
𝑠
K
∈
Ring
∧
K
⊆
ℂ
∧
1
∈
K
77
28
74
76
sylanbrc
⊢
φ
→
K
∈
SubRing
ℂ
fld
78
25
20
77
3jca
⊢
φ
→
F
=
ℂ
fld
↾
𝑠
K
∧
K
=
A
∩
ℂ
∧
K
∈
SubRing
ℂ
fld