pj2f

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

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		incom	$⊢ U \cap T = T \cap U$
11	10 7	eqtrid	$⊢ φ \to U \cap T = \{\underset{˙}{0}\}$
12	4 5 6 8	cntzrecd	$⊢ φ \to U \subseteq Z (T)$
13	1 2 3 4 6 5 11 12 9	pj1f	$⊢ φ \to (U P T) : U \underset{˙}{\oplus} T ⟶ U$
14	2 4	lsmcom2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
15	5 6 8 14	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
16	15	feq2d	$⊢ φ \to ((U P T) : T \underset{˙}{\oplus} U ⟶ U \leftrightarrow (U P T) : U \underset{˙}{\oplus} T ⟶ U)$
17	13 16	mpbird	$⊢ φ \to (U P T) : T \underset{˙}{\oplus} U ⟶ U$

Metamath Proof Explorer