Theorem pj1lid

Description: The left projection function is the identity on the left 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	pj1lid	$$⊢\left(\phi \wedge X\in T\right)\to \left(TPU\right)\left(X\right)=X$$

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