Database
BASIC ALGEBRAIC STRUCTURES
Groups
Direct products
Direct products (extension)
lsmdisjr
Next ⟩
lsmdisj2r
Metamath Proof Explorer
Ascii
Unicode
Theorem
lsmdisjr
Description:
Disjointness from a subgroup sum.
(Contributed by
Mario Carneiro
, 21-Apr-2016)
Ref
Expression
Hypotheses
lsmcntz.p
⊢
⊕
˙
=
LSSum
⁡
G
lsmcntz.s
⊢
φ
→
S
∈
SubGrp
⁡
G
lsmcntz.t
⊢
φ
→
T
∈
SubGrp
⁡
G
lsmcntz.u
⊢
φ
→
U
∈
SubGrp
⁡
G
lsmdisj.o
⊢
0
˙
=
0
G
lsmdisjr.i
⊢
φ
→
S
∩
T
⊕
˙
U
=
0
˙
Assertion
lsmdisjr
⊢
φ
→
S
∩
T
=
0
˙
∧
S
∩
U
=
0
˙
Proof
Step
Hyp
Ref
Expression
1
lsmcntz.p
⊢
⊕
˙
=
LSSum
⁡
G
2
lsmcntz.s
⊢
φ
→
S
∈
SubGrp
⁡
G
3
lsmcntz.t
⊢
φ
→
T
∈
SubGrp
⁡
G
4
lsmcntz.u
⊢
φ
→
U
∈
SubGrp
⁡
G
5
lsmdisj.o
⊢
0
˙
=
0
G
6
lsmdisjr.i
⊢
φ
→
S
∩
T
⊕
˙
U
=
0
˙
7
incom
⊢
S
∩
T
⊕
˙
U
=
T
⊕
˙
U
∩
S
8
7
6
syl5eqr
⊢
φ
→
T
⊕
˙
U
∩
S
=
0
˙
9
1
3
4
2
5
8
lsmdisj
⊢
φ
→
T
∩
S
=
0
˙
∧
U
∩
S
=
0
˙
10
incom
⊢
T
∩
S
=
S
∩
T
11
10
eqeq1i
⊢
T
∩
S
=
0
˙
↔
S
∩
T
=
0
˙
12
incom
⊢
U
∩
S
=
S
∩
U
13
12
eqeq1i
⊢
U
∩
S
=
0
˙
↔
S
∩
U
=
0
˙
14
11
13
anbi12i
⊢
T
∩
S
=
0
˙
∧
U
∩
S
=
0
˙
↔
S
∩
T
=
0
˙
∧
S
∩
U
=
0
˙
15
9
14
sylib
⊢
φ
→
S
∩
T
=
0
˙
∧
S
∩
U
=
0
˙