Theorem pj1eq

Description: Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-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)$$
	pj1eq.5	$$⊢\phi \to X\in \left(T\underset{\dot{}}{\oplus }U\right)$$
	pj1eq.6	$$⊢\phi \to B\in T$$
	pj1eq.7	$$⊢\phi \to C\in U$$
Assertion	pj1eq	$$⊢\phi \to \left(X=B\underset{\dot{}}{+}C\leftrightarrow \left(\left(TPU\right)\left(X\right)=B\wedge \left(UPT\right)\left(X\right)=C\right)\right)$$

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		pj1eq.5	$$⊢\phi \to X\in \left(T\underset{\dot{}}{\oplus }U\right)$$
11		pj1eq.6	$$⊢\phi \to B\in T$$
12		pj1eq.7	$$⊢\phi \to C\in U$$
13	1 2 3 4 5 6 7 8 9	pj1id	$$⊢\left(\phi \wedge X\in \left(T\underset{\dot{}}{\oplus }U\right)\right)\to X=\left(TPU\right)\left(X\right)\underset{\dot{}}{+}\left(UPT\right)\left(X\right)$$
14	10 13	mpdan	$$⊢\phi \to X=\left(TPU\right)\left(X\right)\underset{\dot{}}{+}\left(UPT\right)\left(X\right)$$
15	14	eqeq1d	$$⊢\phi \to \left(X=B\underset{\dot{}}{+}C\leftrightarrow \left(TPU\right)\left(X\right)\underset{\dot{}}{+}\left(UPT\right)\left(X\right)=B\underset{\dot{}}{+}C\right)$$
16	1 2 3 4 5 6 7 8 9	pj1f	$$⊢\phi \to \left(TPU\right):T\underset{\dot{}}{\oplus }U⟶T$$
17	16 10	ffvelrnd	$$⊢\phi \to \left(TPU\right)\left(X\right)\in T$$
18	1 2 3 4 5 6 7 8 9	pj2f	$$⊢\phi \to \left(UPT\right):T\underset{\dot{}}{\oplus }U⟶U$$
19	18 10	ffvelrnd	$$⊢\phi \to \left(UPT\right)\left(X\right)\in U$$
20	1 3 4 5 6 7 8 17 11 19 12	subgdisjb	$$⊢\phi \to \left(\left(TPU\right)\left(X\right)\underset{\dot{}}{+}\left(UPT\right)\left(X\right)=B\underset{\dot{}}{+}C\leftrightarrow \left(\left(TPU\right)\left(X\right)=B\wedge \left(UPT\right)\left(X\right)=C\right)\right)$$
21	15 20	bitrd	$$⊢\phi \to \left(X=B\underset{\dot{}}{+}C\leftrightarrow \left(\left(TPU\right)\left(X\right)=B\wedge \left(UPT\right)\left(X\right)=C\right)\right)$$