Theorem lsmdisj

Description: Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	lsmcntz.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	lsmcntz.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
	lsmcntz.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	lsmcntz.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
	lsmdisj.o	$$⊢\underset{\dot{}}{0}=0_G$$
	lsmdisj.i	$$⊢\phi \to \left(S\underset{\dot{}}{\oplus }T\right)\cap U=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	lsmdisj	$$⊢\phi \to \left(S\cap U=\left\{\underset{\dot{}}{0}\right\}\wedge T\cap U=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsmcntz.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
2		lsmcntz.s	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
3		lsmcntz.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
4		lsmcntz.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
5		lsmdisj.o	$$⊢\underset{\dot{}}{0}=0_G$$
6		lsmdisj.i	$$⊢\phi \to \left(S\underset{\dot{}}{\oplus }T\right)\cap U=\left\{\underset{\dot{}}{0}\right\}$$
7	1	lsmub1	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge T\in \mathrm{SubGrp}\left(G\right)\right)\to S\subseteq S\underset{\dot{}}{\oplus }T$$
8	2 3 7	syl2anc	$$⊢\phi \to S\subseteq S\underset{\dot{}}{\oplus }T$$
9	8	ssrind	$$⊢\phi \to S\cap U\subseteq \left(S\underset{\dot{}}{\oplus }T\right)\cap U$$
10	9 6	sseqtrd	$$⊢\phi \to S\cap U\subseteq \left\{\underset{\dot{}}{0}\right\}$$
11	5	subg0cl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in S$$
12	2 11	syl	$$⊢\phi \to \underset{\dot{}}{0}\in S$$
13	5	subg0cl	$$⊢U\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in U$$
14	4 13	syl	$$⊢\phi \to \underset{\dot{}}{0}\in U$$
15	12 14	elind	$$⊢\phi \to \underset{\dot{}}{0}\in \left(S\cap U\right)$$
16	15	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq S\cap U$$
17	10 16	eqssd	$$⊢\phi \to S\cap U=\left\{\underset{\dot{}}{0}\right\}$$
18	1	lsmub2	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge T\in \mathrm{SubGrp}\left(G\right)\right)\to T\subseteq S\underset{\dot{}}{\oplus }T$$
19	2 3 18	syl2anc	$$⊢\phi \to T\subseteq S\underset{\dot{}}{\oplus }T$$
20	19	ssrind	$$⊢\phi \to T\cap U\subseteq \left(S\underset{\dot{}}{\oplus }T\right)\cap U$$
21	20 6	sseqtrd	$$⊢\phi \to T\cap U\subseteq \left\{\underset{\dot{}}{0}\right\}$$
22	5	subg0cl	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in T$$
23	3 22	syl	$$⊢\phi \to \underset{\dot{}}{0}\in T$$
24	23 14	elind	$$⊢\phi \to \underset{\dot{}}{0}\in \left(T\cap U\right)$$
25	24	snssd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq T\cap U$$
26	21 25	eqssd	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
27	17 26	jca	$$⊢\phi \to \left(S\cap U=\left\{\underset{\dot{}}{0}\right\}\wedge T\cap U=\left\{\underset{\dot{}}{0}\right\}\right)$$