Theorem lsmdisj2r

Description: Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-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\}$$
	lsmdisj2r.i	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	lsmdisj2r	$$⊢\phi \to \left(S\underset{\dot{}}{\oplus }U\right)\cap T=\left\{\underset{\dot{}}{0}\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		lsmdisj2r.i	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
8		eqid	$$⊢{opp}_{𝑔}\left(G\right)={opp}_{𝑔}\left(G\right)$$
9	8 1	oppglsm	$$⊢U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)S=S\underset{\dot{}}{\oplus }U$$
10	9	ineq2i	$$⊢T\cap \left(U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)S\right)=T\cap \left(S\underset{\dot{}}{\oplus }U\right)$$
11		incom	$$⊢T\cap \left(S\underset{\dot{}}{\oplus }U\right)=\left(S\underset{\dot{}}{\oplus }U\right)\cap T$$
12	10 11	eqtri	$$⊢T\cap \left(U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)S\right)=\left(S\underset{\dot{}}{\oplus }U\right)\cap T$$
13		eqid	$$⊢\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)=\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)$$
14	8	oppgsubg	$$⊢\mathrm{SubGrp}\left(G\right)=\mathrm{SubGrp}\left({opp}_{𝑔}\left(G\right)\right)$$
15	4 14	eleqtrdi	$$⊢\phi \to U\in \mathrm{SubGrp}\left({opp}_{𝑔}\left(G\right)\right)$$
16	3 14	eleqtrdi	$$⊢\phi \to T\in \mathrm{SubGrp}\left({opp}_{𝑔}\left(G\right)\right)$$
17	2 14	eleqtrdi	$$⊢\phi \to S\in \mathrm{SubGrp}\left({opp}_{𝑔}\left(G\right)\right)$$
18	8 5	oppgid	$$⊢\underset{\dot{}}{0}=0_{{opp}_{𝑔}\left(G\right)}$$
19	8 1	oppglsm	$$⊢U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)T=T\underset{\dot{}}{\oplus }U$$
20	19	ineq1i	$$⊢\left(U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)T\right)\cap S=\left(T\underset{\dot{}}{\oplus }U\right)\cap S$$
21		incom	$$⊢\left(T\underset{\dot{}}{\oplus }U\right)\cap S=S\cap \left(T\underset{\dot{}}{\oplus }U\right)$$
22	20 21	eqtri	$$⊢\left(U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)T\right)\cap S=S\cap \left(T\underset{\dot{}}{\oplus }U\right)$$
23	22 6	syl5eq	$$⊢\phi \to \left(U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)T\right)\cap S=\left\{\underset{\dot{}}{0}\right\}$$
24		incom	$$⊢T\cap U=U\cap T$$
25	24 7	syl5eqr	$$⊢\phi \to U\cap T=\left\{\underset{\dot{}}{0}\right\}$$
26	13 15 16 17 18 23 25	lsmdisj2	$$⊢\phi \to T\cap \left(U\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)S\right)=\left\{\underset{\dot{}}{0}\right\}$$
27	12 26	syl5eqr	$$⊢\phi \to \left(S\underset{\dot{}}{\oplus }U\right)\cap T=\left\{\underset{\dot{}}{0}\right\}$$