pj1id

Description: Any element of a direct subspace sum can be decomposed into projections onto the left and right factors. (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

	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)$
Assertion	pj1id	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to X = (T P U) (X) \underset{˙}{+} (U P T) (X)$

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		subgrcl	$⊢ T \in SubGrp (G) \to G \in Grp$
11	5 10	syl	$⊢ φ \to G \in Grp$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13	12	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
14	5 13	syl	$⊢ φ \to T \subseteq {Base}_{G}$
15	12	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
16	6 15	syl	$⊢ φ \to U \subseteq {Base}_{G}$
17	11 14 16	3jca	$⊢ φ \to (G \in Grp \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G})$
18	12 1 2 9	pj1val	$⊢ ((G \in Grp \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \land X \in (T \underset{˙}{\oplus} U)) \to (T P U) (X) = (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y)$
19	17 18	sylan	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to (T P U) (X) = (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y)$
20	1 2 3 4 5 6 7 8	pj1eu	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to \exists! x \in T \exists y \in U X = x \underset{˙}{+} y$
21		riotacl2	$⊢ \exists! x \in T \exists y \in U X = x \underset{˙}{+} y \to (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y) \in \{x \in T \| \exists y \in U X = x \underset{˙}{+} y\}$
22	20 21	syl	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to (ι x \in T \| \exists y \in U X = x \underset{˙}{+} y) \in \{x \in T \| \exists y \in U X = x \underset{˙}{+} y\}$
23	19 22	eqeltrd	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to (T P U) (X) \in \{x \in T \| \exists y \in U X = x \underset{˙}{+} y\}$
24		oveq1	$⊢ x = (T P U) (X) \to x \underset{˙}{+} y = (T P U) (X) \underset{˙}{+} y$
25	24	eqeq2d	$⊢ x = (T P U) (X) \to (X = x \underset{˙}{+} y \leftrightarrow X = (T P U) (X) \underset{˙}{+} y)$
26	25	rexbidv	$⊢ x = (T P U) (X) \to (\exists y \in U X = x \underset{˙}{+} y \leftrightarrow \exists y \in U X = (T P U) (X) \underset{˙}{+} y)$
27	26	elrab	$⊢ (T P U) (X) \in \{x \in T \| \exists y \in U X = x \underset{˙}{+} y\} \leftrightarrow ((T P U) (X) \in T \land \exists y \in U X = (T P U) (X) \underset{˙}{+} y)$
28	27	simprbi	$⊢ (T P U) (X) \in \{x \in T \| \exists y \in U X = x \underset{˙}{+} y\} \to \exists y \in U X = (T P U) (X) \underset{˙}{+} y$
29	23 28	syl	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to \exists y \in U X = (T P U) (X) \underset{˙}{+} y$
30		simprr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to X = (T P U) (X) \underset{˙}{+} y$
31	11	ad2antrr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to G \in Grp$
32	16	ad2antrr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to U \subseteq {Base}_{G}$
33	14	ad2antrr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to T \subseteq {Base}_{G}$
34		simplr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to X \in (T \underset{˙}{\oplus} U)$
35	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$
36	5 6 8 35	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
37	36	ad2antrr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
38	34 37	eleqtrd	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to X \in (U \underset{˙}{\oplus} T)$
39	12 1 2 9	pj1val	$⊢ ((G \in Grp \land U \subseteq {Base}_{G} \land T \subseteq {Base}_{G}) \land X \in (U \underset{˙}{\oplus} T)) \to (U P T) (X) = (ι u \in U \| \exists v \in T X = u \underset{˙}{+} v)$
40	31 32 33 38 39	syl31anc	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (U P T) (X) = (ι u \in U \| \exists v \in T X = u \underset{˙}{+} v)$
41	1 2 3 4 5 6 7 8 9	pj1f	$⊢ φ \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$
42	41	ad2antrr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$
43	42 34	ffvelrnd	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (T P U) (X) \in T$
44	8	ad2antrr	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to T \subseteq Z (U)$
45	44 43	sseldd	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (T P U) (X) \in Z (U)$
46		simprl	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to y \in U$
47	1 4	cntzi	$⊢ ((T P U) (X) \in Z (U) \land y \in U) \to (T P U) (X) \underset{˙}{+} y = y \underset{˙}{+} (T P U) (X)$
48	45 46 47	syl2anc	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (T P U) (X) \underset{˙}{+} y = y \underset{˙}{+} (T P U) (X)$
49	30 48	eqtrd	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to X = y \underset{˙}{+} (T P U) (X)$
50		oveq2	$⊢ v = (T P U) (X) \to y \underset{˙}{+} v = y \underset{˙}{+} (T P U) (X)$
51	50	rspceeqv	$⊢ ((T P U) (X) \in T \land X = y \underset{˙}{+} (T P U) (X)) \to \exists v \in T X = y \underset{˙}{+} v$
52	43 49 51	syl2anc	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to \exists v \in T X = y \underset{˙}{+} v$
53		simpll	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to φ$
54		incom	$⊢ U \cap T = T \cap U$
55	54 7	eqtrid	$⊢ φ \to U \cap T = \{\underset{˙}{0}\}$
56	4 5 6 8	cntzrecd	$⊢ φ \to U \subseteq Z (T)$
57	1 2 3 4 6 5 55 56	pj1eu	$⊢ (φ \land X \in (U \underset{˙}{\oplus} T)) \to \exists! u \in U \exists v \in T X = u \underset{˙}{+} v$
58	53 38 57	syl2anc	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to \exists! u \in U \exists v \in T X = u \underset{˙}{+} v$
59		oveq1	$⊢ u = y \to u \underset{˙}{+} v = y \underset{˙}{+} v$
60	59	eqeq2d	$⊢ u = y \to (X = u \underset{˙}{+} v \leftrightarrow X = y \underset{˙}{+} v)$
61	60	rexbidv	$⊢ u = y \to (\exists v \in T X = u \underset{˙}{+} v \leftrightarrow \exists v \in T X = y \underset{˙}{+} v)$
62	61	riota2	$⊢ (y \in U \land \exists! u \in U \exists v \in T X = u \underset{˙}{+} v) \to (\exists v \in T X = y \underset{˙}{+} v \leftrightarrow (ι u \in U \| \exists v \in T X = u \underset{˙}{+} v) = y)$
63	46 58 62	syl2anc	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (\exists v \in T X = y \underset{˙}{+} v \leftrightarrow (ι u \in U \| \exists v \in T X = u \underset{˙}{+} v) = y)$
64	52 63	mpbid	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (ι u \in U \| \exists v \in T X = u \underset{˙}{+} v) = y$
65	40 64	eqtrd	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (U P T) (X) = y$
66	65	oveq2d	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to (T P U) (X) \underset{˙}{+} (U P T) (X) = (T P U) (X) \underset{˙}{+} y$
67	30 66	eqtr4d	$⊢ ((φ \land X \in (T \underset{˙}{\oplus} U)) \land (y \in U \land X = (T P U) (X) \underset{˙}{+} y)) \to X = (T P U) (X) \underset{˙}{+} (U P T) (X)$
68	29 67	rexlimddv	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to X = (T P U) (X) \underset{˙}{+} (U P T) (X)$

Metamath Proof Explorer

Theorem pj1id

Proof