grpraddf1o

Description: Right addition by a group element is a bijection on any group. (Contributed by SN, 28-Apr-2012)

	Ref	Expression
Hypotheses	grpraddf1o.b	$⊢ B = {Base}_{G}$
	grpraddf1o.p	$⊢ \underset{˙}{+} = +_{G}$
	grpraddf1o.n	$⊢ F = (x \in B ⟼ x \underset{˙}{+} X)$
Assertion	grpraddf1o	$⊢ (G \in Grp \land X \in B) \to F : B \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		grpraddf1o.b	$⊢ B = {Base}_{G}$
2		grpraddf1o.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpraddf1o.n	$⊢ F = (x \in B ⟼ x \underset{˙}{+} X)$
4		simpll	$⊢ ((G \in Grp \land X \in B) \land x \in B) \to G \in Grp$
5		simpr	$⊢ ((G \in Grp \land X \in B) \land x \in B) \to x \in B$
6		simplr	$⊢ ((G \in Grp \land X \in B) \land x \in B) \to X \in B$
7	1 2 4 5 6	grpcld	$⊢ ((G \in Grp \land X \in B) \land x \in B) \to x \underset{˙}{+} X \in B$
8		simpll	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to G \in Grp$
9		simpr	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to y \in B$
10		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
11		simplr	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to X \in B$
12	1 10 8 11	grpinvcld	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to {inv}_{g} (G) (X) \in B$
13	1 2 8 9 12	grpcld	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to y \underset{˙}{+} {inv}_{g} (G) (X) \in B$
14		eqcom	$⊢ x = y \underset{˙}{+} {inv}_{g} (G) (X) \leftrightarrow y \underset{˙}{+} {inv}_{g} (G) (X) = x$
15		simpll	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to G \in Grp$
16	13	adantrl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to y \underset{˙}{+} {inv}_{g} (G) (X) \in B$
17		simprl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to x \in B$
18		simplr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to X \in B$
19	1 2	grprcan	$⊢ (G \in Grp \land (y \underset{˙}{+} {inv}_{g} (G) (X) \in B \land x \in B \land X \in B)) \to ((y \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = x \underset{˙}{+} X \leftrightarrow y \underset{˙}{+} {inv}_{g} (G) (X) = x)$
20	15 16 17 18 19	syl13anc	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to ((y \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = x \underset{˙}{+} X \leftrightarrow y \underset{˙}{+} {inv}_{g} (G) (X) = x)$
21		simprr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to y \in B$
22	12	adantrl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to {inv}_{g} (G) (X) \in B$
23	1 2 15 21 22 18	grpassd	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (y \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = y \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} X)$
24		eqid	$⊢ 0_{G} = 0_{G}$
25	1 2 24 10	grplinv	$⊢ (G \in Grp \land X \in B) \to {inv}_{g} (G) (X) \underset{˙}{+} X = 0_{G}$
26	25	adantr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to {inv}_{g} (G) (X) \underset{˙}{+} X = 0_{G}$
27	26	oveq2d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to y \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} X) = y \underset{˙}{+} 0_{G}$
28	1 2 24	grprid	$⊢ (G \in Grp \land y \in B) \to y \underset{˙}{+} 0_{G} = y$
29	28	ad2ant2rl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to y \underset{˙}{+} 0_{G} = y$
30	23 27 29	3eqtrd	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (y \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = y$
31	30	eqeq1d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to ((y \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = x \underset{˙}{+} X \leftrightarrow y = x \underset{˙}{+} X)$
32	20 31	bitr3d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (y \underset{˙}{+} {inv}_{g} (G) (X) = x \leftrightarrow y = x \underset{˙}{+} X)$
33	14 32	bitrid	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (x = y \underset{˙}{+} {inv}_{g} (G) (X) \leftrightarrow y = x \underset{˙}{+} X)$
34	3 7 13 33	f1o2d	$⊢ (G \in Grp \land X \in B) \to F : B \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem grpraddf1o

Proof