Metamath Proof Explorer


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 eqtr3id φ 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 ˙