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{˙}{+} = +_{G}$
	pj1eu.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	pj1eu.o	$⊢ \underset{˙}{0} = 0_{G}$
	pj1eu.z	$⊢ Z = Cntz (G)$
	pj1eu.2	$⊢ φ \to T \in SubGrp (G)$
	pj1eu.3	$⊢ φ \to U \in SubGrp (G)$
	pj1eu.4	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
	pj1eu.5	$⊢ φ \to T \subseteq Z (U)$
	pj1f.p	$⊢ P = {proj}_{1} (G)$
	pj1eq.5	$⊢ φ \to X \in (T \underset{˙}{\oplus} U)$
	pj1eq.6	$⊢ φ \to B \in T$
	pj1eq.7	$⊢ φ \to C \in U$
Assertion	pj1eq	$⊢ φ \to (X = B \underset{˙}{+} C \leftrightarrow ((T P U) (X) = B \land (U P T) (X) = C))$

Proof

Step	Hyp	Ref	Expression
1		pj1eu.a	$⊢ \underset{˙}{+} = +_{G}$
2		pj1eu.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		pj1eu.o	$⊢ \underset{˙}{0} = 0_{G}$
4		pj1eu.z	$⊢ Z = Cntz (G)$
5		pj1eu.2	$⊢ φ \to T \in SubGrp (G)$
6		pj1eu.3	$⊢ φ \to U \in SubGrp (G)$
7		pj1eu.4	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
8		pj1eu.5	$⊢ φ \to T \subseteq Z (U)$
9		pj1f.p	$⊢ P = {proj}_{1} (G)$
10		pj1eq.5	$⊢ φ \to X \in (T \underset{˙}{\oplus} U)$
11		pj1eq.6	$⊢ φ \to B \in T$
12		pj1eq.7	$⊢ φ \to C \in U$
13	1 2 3 4 5 6 7 8 9	pj1id	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to X = (T P U) (X) \underset{˙}{+} (U P T) (X)$
14	10 13	mpdan	$⊢ φ \to X = (T P U) (X) \underset{˙}{+} (U P T) (X)$
15	14	eqeq1d	$⊢ φ \to (X = B \underset{˙}{+} C \leftrightarrow (T P U) (X) \underset{˙}{+} (U P T) (X) = B \underset{˙}{+} C)$
16	1 2 3 4 5 6 7 8 9	pj1f	$⊢ φ \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$
17	16 10	ffvelcdmd	$⊢ φ \to (T P U) (X) \in T$
18	1 2 3 4 5 6 7 8 9	pj2f	$⊢ φ \to (U P T) : T \underset{˙}{\oplus} U ⟶ U$
19	18 10	ffvelcdmd	$⊢ φ \to (U P T) (X) \in U$
20	1 3 4 5 6 7 8 17 11 19 12	subgdisjb	$⊢ φ \to ((T P U) (X) \underset{˙}{+} (U P T) (X) = B \underset{˙}{+} C \leftrightarrow ((T P U) (X) = B \land (U P T) (X) = C))$
21	15 20	bitrd	$⊢ φ \to (X = B \underset{˙}{+} C \leftrightarrow ((T P U) (X) = B \land (U P T) (X) = C))$

Metamath Proof Explorer

Theorem pj1eq

Proof