Metamath Proof Explorer


Theorem lsmdisj3b

Description: Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses lsmcntz.p ˙=LSSumG
lsmcntz.s φSSubGrpG
lsmcntz.t φTSubGrpG
lsmcntz.u φUSubGrpG
lsmdisj.o 0˙=0G
lsmdisj3b.z Z=CntzG
lsmdisj3b.2 φTZU
Assertion lsmdisj3b φS˙TU=0˙ST=0˙ST˙U=0˙TU=0˙

Proof

Step Hyp Ref Expression
1 lsmcntz.p ˙=LSSumG
2 lsmcntz.s φSSubGrpG
3 lsmcntz.t φTSubGrpG
4 lsmcntz.u φUSubGrpG
5 lsmdisj.o 0˙=0G
6 lsmdisj3b.z Z=CntzG
7 lsmdisj3b.2 φTZU
8 1 2 4 3 5 lsmdisj2b φS˙TU=0˙ST=0˙SU˙T=0˙UT=0˙
9 1 6 lsmcom2 TSubGrpGUSubGrpGTZUT˙U=U˙T
10 3 4 7 9 syl3anc φT˙U=U˙T
11 10 ineq2d φST˙U=SU˙T
12 11 eqeq1d φST˙U=0˙SU˙T=0˙
13 incom TU=UT
14 13 a1i φTU=UT
15 14 eqeq1d φTU=0˙UT=0˙
16 12 15 anbi12d φST˙U=0˙TU=0˙SU˙T=0˙UT=0˙
17 8 16 bitr4d φS˙TU=0˙ST=0˙ST˙U=0˙TU=0˙