pj1eu

Description: Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-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)$
Assertion	pj1eu	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to \exists! x \in T \exists y \in U X = x \underset{˙}{+} y$

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	1 2	lsmelval	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists x \in T \exists y \in U X = x \underset{˙}{+} y)$
10	5 6 9	syl2anc	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists x \in T \exists y \in U X = x \underset{˙}{+} y)$
11	10	biimpa	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to \exists x \in T \exists y \in U X = x \underset{˙}{+} y$
12		reeanv	$⊢ \exists y \in U \exists v \in U (X = x \underset{˙}{+} y \land X = u \underset{˙}{+} v) \leftrightarrow (\exists y \in U X = x \underset{˙}{+} y \land \exists v \in U X = u \underset{˙}{+} v)$
13		eqtr2	$⊢ (X = x \underset{˙}{+} y \land X = u \underset{˙}{+} v) \to x \underset{˙}{+} y = u \underset{˙}{+} v$
14	5	ad2antrr	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to T \in SubGrp (G)$
15	6	ad2antrr	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to U \in SubGrp (G)$
16	7	ad2antrr	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to T \cap U = \{\underset{˙}{0}\}$
17	8	ad2antrr	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to T \subseteq Z (U)$
18		simplrl	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to x \in T$
19		simplrr	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to u \in T$
20		simprl	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to y \in U$
21		simprr	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to v \in U$
22	1 3 4 14 15 16 17 18 19 20 21	subgdisjb	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to (x \underset{˙}{+} y = u \underset{˙}{+} v \leftrightarrow (x = u \land y = v))$
23		simpl	$⊢ (x = u \land y = v) \to x = u$
24	22 23	biimtrdi	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to (x \underset{˙}{+} y = u \underset{˙}{+} v \to x = u)$
25	13 24	syl5	$⊢ ((φ \land (x \in T \land u \in T)) \land (y \in U \land v \in U)) \to ((X = x \underset{˙}{+} y \land X = u \underset{˙}{+} v) \to x = u)$
26	25	rexlimdvva	$⊢ (φ \land (x \in T \land u \in T)) \to (\exists y \in U \exists v \in U (X = x \underset{˙}{+} y \land X = u \underset{˙}{+} v) \to x = u)$
27	12 26	biimtrrid	$⊢ (φ \land (x \in T \land u \in T)) \to ((\exists y \in U X = x \underset{˙}{+} y \land \exists v \in U X = u \underset{˙}{+} v) \to x = u)$
28	27	ralrimivva	$⊢ φ \to \forall x \in T \forall u \in T ((\exists y \in U X = x \underset{˙}{+} y \land \exists v \in U X = u \underset{˙}{+} v) \to x = u)$
29	28	adantr	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to \forall x \in T \forall u \in T ((\exists y \in U X = x \underset{˙}{+} y \land \exists v \in U X = u \underset{˙}{+} v) \to x = u)$
30		oveq1	$⊢ x = u \to x \underset{˙}{+} y = u \underset{˙}{+} y$
31	30	eqeq2d	$⊢ x = u \to (X = x \underset{˙}{+} y \leftrightarrow X = u \underset{˙}{+} y)$
32	31	rexbidv	$⊢ x = u \to (\exists y \in U X = x \underset{˙}{+} y \leftrightarrow \exists y \in U X = u \underset{˙}{+} y)$
33		oveq2	$⊢ y = v \to u \underset{˙}{+} y = u \underset{˙}{+} v$
34	33	eqeq2d	$⊢ y = v \to (X = u \underset{˙}{+} y \leftrightarrow X = u \underset{˙}{+} v)$
35	34	cbvrexvw	$⊢ \exists y \in U X = u \underset{˙}{+} y \leftrightarrow \exists v \in U X = u \underset{˙}{+} v$
36	32 35	bitrdi	$⊢ x = u \to (\exists y \in U X = x \underset{˙}{+} y \leftrightarrow \exists v \in U X = u \underset{˙}{+} v)$
37	36	reu4	$⊢ \exists! x \in T \exists y \in U X = x \underset{˙}{+} y \leftrightarrow (\exists x \in T \exists y \in U X = x \underset{˙}{+} y \land \forall x \in T \forall u \in T ((\exists y \in U X = x \underset{˙}{+} y \land \exists v \in U X = u \underset{˙}{+} v) \to x = u))$
38	11 29 37	sylanbrc	$⊢ (φ \land X \in (T \underset{˙}{\oplus} U)) \to \exists! x \in T \exists y \in U X = x \underset{˙}{+} y$

Metamath Proof Explorer

Theorem pj1eu

Proof