subgdisjb

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth , this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-Jul-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	subgdisj.p	$⊢ \underset{˙}{+} = +_{G}$
	subgdisj.o	$⊢ \underset{˙}{0} = 0_{G}$
	subgdisj.z	$⊢ Z = Cntz (G)$
	subgdisj.t	$⊢ φ \to T \in SubGrp (G)$
	subgdisj.u	$⊢ φ \to U \in SubGrp (G)$
	subgdisj.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
	subgdisj.s	$⊢ φ \to T \subseteq Z (U)$
	subgdisj.a	$⊢ φ \to A \in T$
	subgdisj.c	$⊢ φ \to C \in T$
	subgdisj.b	$⊢ φ \to B \in U$
	subgdisj.d	$⊢ φ \to D \in U$
Assertion	subgdisjb	$⊢ φ \to (A \underset{˙}{+} B = C \underset{˙}{+} D \leftrightarrow (A = C \land B = D))$

Proof

Step	Hyp	Ref	Expression
1		subgdisj.p	$⊢ \underset{˙}{+} = +_{G}$
2		subgdisj.o	$⊢ \underset{˙}{0} = 0_{G}$
3		subgdisj.z	$⊢ Z = Cntz (G)$
4		subgdisj.t	$⊢ φ \to T \in SubGrp (G)$
5		subgdisj.u	$⊢ φ \to U \in SubGrp (G)$
6		subgdisj.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
7		subgdisj.s	$⊢ φ \to T \subseteq Z (U)$
8		subgdisj.a	$⊢ φ \to A \in T$
9		subgdisj.c	$⊢ φ \to C \in T$
10		subgdisj.b	$⊢ φ \to B \in U$
11		subgdisj.d	$⊢ φ \to D \in U$
12	4	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to T \in SubGrp (G)$
13	5	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to U \in SubGrp (G)$
14	6	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to T \cap U = \{\underset{˙}{0}\}$
15	7	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to T \subseteq Z (U)$
16	8	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to A \in T$
17	9	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to C \in T$
18	10	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to B \in U$
19	11	adantr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to D \in U$
20		simpr	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to A \underset{˙}{+} B = C \underset{˙}{+} D$
21	1 2 3 12 13 14 15 16 17 18 19 20	subgdisj1	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to A = C$
22	1 2 3 12 13 14 15 16 17 18 19 20	subgdisj2	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to B = D$
23	21 22	jca	$⊢ (φ \land A \underset{˙}{+} B = C \underset{˙}{+} D) \to (A = C \land B = D)$
24	23	ex	$⊢ φ \to (A \underset{˙}{+} B = C \underset{˙}{+} D \to (A = C \land B = D))$
25		oveq12	$⊢ (A = C \land B = D) \to A \underset{˙}{+} B = C \underset{˙}{+} D$
26	24 25	impbid1	$⊢ φ \to (A \underset{˙}{+} B = C \underset{˙}{+} D \leftrightarrow (A = C \land B = D))$

Metamath Proof Explorer

Theorem subgdisjb

Proof