Theorem pj2f

Description: The right projection function maps a direct subspace sum onto the right factor. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	pj1eu.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	pj1eu.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	pj1eu.o	$$⊢\underset{\dot{}}{0}=0_G$$
	pj1eu.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	pj1eu.2	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	pj1eu.3	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
	pj1eu.4	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
	pj1eu.5	$$⊢\phi \to T\subseteq Z\left(U\right)$$
	pj1f.p	$$⊢P={proj}_1\left(G\right)$$
Assertion	pj2f	$$⊢\phi \to \left(UPT\right):T\underset{\dot{}}{\oplus }U⟶U$$

Proof

Step	Hyp	Ref	Expression
1		pj1eu.a	$$⊢\underset{\dot{}}{+}={+}_G$$
2		pj1eu.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
3		pj1eu.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		pj1eu.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
5		pj1eu.2	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
6		pj1eu.3	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
7		pj1eu.4	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
8		pj1eu.5	$$⊢\phi \to T\subseteq Z\left(U\right)$$
9		pj1f.p	$$⊢P={proj}_1\left(G\right)$$
10		incom	$$⊢U\cap T=T\cap U$$
11	10 7	syl5eq	$$⊢\phi \to U\cap T=\left\{\underset{\dot{}}{0}\right\}$$
12	4 5 6 8	cntzrecd	$$⊢\phi \to U\subseteq Z\left(T\right)$$
13	1 2 3 4 6 5 11 12 9	pj1f	$$⊢\phi \to \left(UPT\right):U\underset{\dot{}}{\oplus }T⟶U$$
14	2 4	lsmcom2	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge U\in \mathrm{SubGrp}\left(G\right)\wedge T\subseteq Z\left(U\right)\right)\to T\underset{\dot{}}{\oplus }U=U\underset{\dot{}}{\oplus }T$$
15	5 6 8 14	syl3anc	$$⊢\phi \to T\underset{\dot{}}{\oplus }U=U\underset{\dot{}}{\oplus }T$$
16	15	feq2d	$$⊢\phi \to \left(\left(UPT\right):T\underset{\dot{}}{\oplus }U⟶U\leftrightarrow \left(UPT\right):U\underset{\dot{}}{\oplus }T⟶U\right)$$
17	13 16	mpbird	$$⊢\phi \to \left(UPT\right):T\underset{\dot{}}{\oplus }U⟶U$$