Theorem pj1rid

Description: The left projection function is the zero operator on the right subspace. (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	pj1rid	$$⊢\left(\phi \wedge X\in U\right)\to \left(TPU\right)\left(X\right)=\underset{\dot{}}{0}$$

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	5	adantr	$$⊢\left(\phi \wedge X\in U\right)\to T\in \mathrm{SubGrp}\left(G\right)$$
11		subgrcl	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
12	10 11	syl	$$⊢\left(\phi \wedge X\in U\right)\to G\in \mathrm{Grp}$$
13		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
14	13	subgss	$$⊢U\in \mathrm{SubGrp}\left(G\right)\to U\subseteq {\mathrm{Base}}_G$$
15	6 14	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_G$$
16	15	sselda	$$⊢\left(\phi \wedge X\in U\right)\to X\in {\mathrm{Base}}_G$$
17	13 1 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in {\mathrm{Base}}_G\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
18	12 16 17	syl2anc	$$⊢\left(\phi \wedge X\in U\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
19	18	eqcomd	$$⊢\left(\phi \wedge X\in U\right)\to X=\underset{\dot{}}{0}\underset{\dot{}}{+}X$$
20	6	adantr	$$⊢\left(\phi \wedge X\in U\right)\to U\in \mathrm{SubGrp}\left(G\right)$$
21	7	adantr	$$⊢\left(\phi \wedge X\in U\right)\to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
22	8	adantr	$$⊢\left(\phi \wedge X\in U\right)\to T\subseteq Z\left(U\right)$$
23	2	lsmub2	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge U\in \mathrm{SubGrp}\left(G\right)\right)\to U\subseteq T\underset{\dot{}}{\oplus }U$$
24	5 6 23	syl2anc	$$⊢\phi \to U\subseteq T\underset{\dot{}}{\oplus }U$$
25	24	sselda	$$⊢\left(\phi \wedge X\in U\right)\to X\in \left(T\underset{\dot{}}{\oplus }U\right)$$
26	3	subg0cl	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{0}\in T$$
27	10 26	syl	$$⊢\left(\phi \wedge X\in U\right)\to \underset{\dot{}}{0}\in T$$
28		simpr	$$⊢\left(\phi \wedge X\in U\right)\to X\in U$$
29	1 2 3 4 10 20 21 22 9 25 27 28	pj1eq	$$⊢\left(\phi \wedge X\in U\right)\to \left(X=\underset{\dot{}}{0}\underset{\dot{}}{+}X\leftrightarrow \left(\left(TPU\right)\left(X\right)=\underset{\dot{}}{0}\wedge \left(UPT\right)\left(X\right)=X\right)\right)$$
30	19 29	mpbid	$$⊢\left(\phi \wedge X\in U\right)\to \left(\left(TPU\right)\left(X\right)=\underset{\dot{}}{0}\wedge \left(UPT\right)\left(X\right)=X\right)$$
31	30	simpld	$$⊢\left(\phi \wedge X\in U\right)\to \left(TPU\right)\left(X\right)=\underset{\dot{}}{0}$$