Theorem lsmdisjr

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$$
	lsmdisjr.i	$$⊢\phi \to S\cap \left(T\underset{\dot{}}{\oplus }U\right)=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	lsmdisjr	$$⊢\phi \to \left(S\cap T=\left\{\underset{\dot{}}{0}\right\}\wedge S\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		lsmdisjr.i	$$⊢\phi \to S\cap \left(T\underset{\dot{}}{\oplus }U\right)=\left\{\underset{\dot{}}{0}\right\}$$
7		incom	$$⊢S\cap \left(T\underset{\dot{}}{\oplus }U\right)=\left(T\underset{\dot{}}{\oplus }U\right)\cap S$$
8	7 6	eqtr3id	$$⊢\phi \to \left(T\underset{\dot{}}{\oplus }U\right)\cap S=\left\{\underset{\dot{}}{0}\right\}$$
9	1 3 4 2 5 8	lsmdisj	$$⊢\phi \to \left(T\cap S=\left\{\underset{\dot{}}{0}\right\}\wedge U\cap S=\left\{\underset{\dot{}}{0}\right\}\right)$$
10		incom	$$⊢T\cap S=S\cap T$$
11	10	eqeq1i	$$⊢T\cap S=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow S\cap T=\left\{\underset{\dot{}}{0}\right\}$$
12		incom	$$⊢U\cap S=S\cap U$$
13	12	eqeq1i	$$⊢U\cap S=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow S\cap U=\left\{\underset{\dot{}}{0}\right\}$$
14	11 13	anbi12i	$$⊢\left(T\cap S=\left\{\underset{\dot{}}{0}\right\}\wedge U\cap S=\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(S\cap T=\left\{\underset{\dot{}}{0}\right\}\wedge S\cap U=\left\{\underset{\dot{}}{0}\right\}\right)$$
15	9 14	sylib	$$⊢\phi \to \left(S\cap T=\left\{\underset{\dot{}}{0}\right\}\wedge S\cap U=\left\{\underset{\dot{}}{0}\right\}\right)$$