Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Division Ring Extensions
drgextgsum
Next ⟩
Vector Spaces
Metamath Proof Explorer
Ascii
Unicode
Theorem
drgextgsum
Description:
Group sum in a division ring extension.
(Contributed by
Thierry Arnoux
, 17-Jul-2023)
Ref
Expression
Hypotheses
drgext.b
⊢
B
=
subringAlg
⁡
E
⁡
U
drgext.1
⊢
φ
→
E
∈
DivRing
drgext.2
⊢
φ
→
U
∈
SubRing
⁡
E
drgext.f
⊢
F
=
E
↾
𝑠
U
drgext.3
⊢
φ
→
F
∈
DivRing
drgextgsum.1
⊢
φ
→
X
∈
V
Assertion
drgextgsum
⊢
φ
→
∑
E
i
∈
X
Y
=
∑
B
i
∈
X
Y
Proof
Step
Hyp
Ref
Expression
1
drgext.b
⊢
B
=
subringAlg
⁡
E
⁡
U
2
drgext.1
⊢
φ
→
E
∈
DivRing
3
drgext.2
⊢
φ
→
U
∈
SubRing
⁡
E
4
drgext.f
⊢
F
=
E
↾
𝑠
U
5
drgext.3
⊢
φ
→
F
∈
DivRing
6
drgextgsum.1
⊢
φ
→
X
∈
V
7
6
mptexd
⊢
φ
→
i
∈
X
⟼
Y
∈
V
8
1
4
sralvec
⊢
E
∈
DivRing
∧
F
∈
DivRing
∧
U
∈
SubRing
⁡
E
→
B
∈
LVec
9
2
5
3
8
syl3anc
⊢
φ
→
B
∈
LVec
10
eqid
⊢
Base
E
=
Base
E
11
10
subrgss
⊢
U
∈
SubRing
⁡
E
→
U
⊆
Base
E
12
3
11
syl
⊢
φ
→
U
⊆
Base
E
13
1
7
2
9
12
gsumsra
⊢
φ
→
∑
E
i
∈
X
Y
=
∑
B
i
∈
X
Y