grplmulf1o

Description: Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		grplmulf1o.b	$⊢ B = {Base}_{G}$
2		grplmulf1o.p	$⊢ \underset{˙}{+} = +_{G}$
3		grplmulf1o.n	$⊢ F = (x \in B ⟼ X \underset{˙}{+} x)$
4	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land x \in B) \to X \underset{˙}{+} x \in B$
5	4	3expa	$⊢ ((G \in Grp \land X \in B) \land x \in B) \to X \underset{˙}{+} x \in B$
6		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
7	1 6	grpinvcl	$⊢ (G \in Grp \land X \in B) \to {inv}_{g} (G) (X) \in B$
8	1 2	grpcl	$⊢ (G \in Grp \land {inv}_{g} (G) (X) \in B \land y \in B) \to {inv}_{g} (G) (X) \underset{˙}{+} y \in B$
9	8	3expa	$⊢ ((G \in Grp \land {inv}_{g} (G) (X) \in B) \land y \in B) \to {inv}_{g} (G) (X) \underset{˙}{+} y \in B$
10	7 9	syldanl	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to {inv}_{g} (G) (X) \underset{˙}{+} y \in B$
11		eqcom	$⊢ x = {inv}_{g} (G) (X) \underset{˙}{+} y \leftrightarrow {inv}_{g} (G) (X) \underset{˙}{+} y = x$
12		simpll	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to G \in Grp$
13	10	adantrl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to {inv}_{g} (G) (X) \underset{˙}{+} y \in B$
14		simprl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to x \in B$
15		simplr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to X \in B$
16	1 2	grplcan	$⊢ (G \in Grp \land ({inv}_{g} (G) (X) \underset{˙}{+} y \in B \land x \in B \land X \in B)) \to (X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} y) = X \underset{˙}{+} x \leftrightarrow {inv}_{g} (G) (X) \underset{˙}{+} y = x)$
17	12 13 14 15 16	syl13anc	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} y) = X \underset{˙}{+} x \leftrightarrow {inv}_{g} (G) (X) \underset{˙}{+} y = x)$
18		eqid	$⊢ 0_{G} = 0_{G}$
19	1 2 18 6	grprinv	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} {inv}_{g} (G) (X) = 0_{G}$
20	19	adantr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to X \underset{˙}{+} {inv}_{g} (G) (X) = 0_{G}$
21	20	oveq1d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (X \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} y = 0_{G} \underset{˙}{+} y$
22	7	adantr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to {inv}_{g} (G) (X) \in B$
23		simprr	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to y \in B$
24	1 2	grpass	$⊢ (G \in Grp \land (X \in B \land {inv}_{g} (G) (X) \in B \land y \in B)) \to (X \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} y = X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} y)$
25	12 15 22 23 24	syl13anc	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (X \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} y = X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} y)$
26	1 2 18	grplid	$⊢ (G \in Grp \land y \in B) \to 0_{G} \underset{˙}{+} y = y$
27	26	ad2ant2rl	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to 0_{G} \underset{˙}{+} y = y$
28	21 25 27	3eqtr3d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} y) = y$
29	28	eqeq1d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} y) = X \underset{˙}{+} x \leftrightarrow y = X \underset{˙}{+} x)$
30	17 29	bitr3d	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to ({inv}_{g} (G) (X) \underset{˙}{+} y = x \leftrightarrow y = X \underset{˙}{+} x)$
31	11 30	syl5bb	$⊢ ((G \in Grp \land X \in B) \land (x \in B \land y \in B)) \to (x = {inv}_{g} (G) (X) \underset{˙}{+} y \leftrightarrow y = X \underset{˙}{+} x)$
32	3 5 10 31	f1o2d	$⊢ (G \in Grp \land X \in B) \to F : B \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem grplmulf1o

Proof