lactghmga

Description: The converse of galactghm . The uncurrying of a homomorphism into ( SymGrpY ) is a group action. Thus, group actions and group homomorphisms into a symmetric group are essentially equivalent notions. (Contributed by Mario Carneiro, 15-Jan-2015)

	Ref	Expression
Hypotheses	lactghmga.x	$⊢ X = {Base}_{G}$
	lactghmga.h	$⊢ H = SymGrp (Y)$
	lactghmga.f	$⊢ \underset{˙}{\oplus} = (x \in X, y \in Y ⟼ F (x) (y))$
Assertion	lactghmga	$⊢ F \in (G GrpHom H) \to \underset{˙}{\oplus} \in (G GrpAct Y)$

Proof

Step	Hyp	Ref	Expression
1		lactghmga.x	$⊢ X = {Base}_{G}$
2		lactghmga.h	$⊢ H = SymGrp (Y)$
3		lactghmga.f	$⊢ \underset{˙}{\oplus} = (x \in X, y \in Y ⟼ F (x) (y))$
4		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
5		ghmgrp2	$⊢ F \in (G GrpHom H) \to H \in Grp$
6		grpn0	$⊢ H \in Grp \to H \neq \emptyset$
7		fvprc	$⊢ \neg Y \in V \to SymGrp (Y) = \emptyset$
8	2 7	eqtrid	$⊢ \neg Y \in V \to H = \emptyset$
9	8	necon1ai	$⊢ H \neq \emptyset \to Y \in V$
10	5 6 9	3syl	$⊢ F \in (G GrpHom H) \to Y \in V$
11		eqid	$⊢ {Base}_{H} = {Base}_{H}$
12	1 11	ghmf	$⊢ F \in (G GrpHom H) \to F : X ⟶ {Base}_{H}$
13	12	ffvelcdmda	$⊢ (F \in (G GrpHom H) \land x \in X) \to F (x) \in {Base}_{H}$
14	10	adantr	$⊢ (F \in (G GrpHom H) \land x \in X) \to Y \in V$
15	2 11	elsymgbas	$⊢ Y \in V \to (F (x) \in {Base}_{H} \leftrightarrow F (x) : Y \underset{1-1 onto}{⟶} Y)$
16	14 15	syl	$⊢ (F \in (G GrpHom H) \land x \in X) \to (F (x) \in {Base}_{H} \leftrightarrow F (x) : Y \underset{1-1 onto}{⟶} Y)$
17	13 16	mpbid	$⊢ (F \in (G GrpHom H) \land x \in X) \to F (x) : Y \underset{1-1 onto}{⟶} Y$
18		f1of	$⊢ F (x) : Y \underset{1-1 onto}{⟶} Y \to F (x) : Y ⟶ Y$
19	17 18	syl	$⊢ (F \in (G GrpHom H) \land x \in X) \to F (x) : Y ⟶ Y$
20	19	ffvelcdmda	$⊢ ((F \in (G GrpHom H) \land x \in X) \land y \in Y) \to F (x) (y) \in Y$
21	20	ralrimiva	$⊢ (F \in (G GrpHom H) \land x \in X) \to \forall y \in Y F (x) (y) \in Y$
22	21	ralrimiva	$⊢ F \in (G GrpHom H) \to \forall x \in X \forall y \in Y F (x) (y) \in Y$
23	3	fmpo	$⊢ \forall x \in X \forall y \in Y F (x) (y) \in Y \leftrightarrow \underset{˙}{\oplus} : X \times Y ⟶ Y$
24	22 23	sylib	$⊢ F \in (G GrpHom H) \to \underset{˙}{\oplus} : X \times Y ⟶ Y$
25		eqid	$⊢ 0_{G} = 0_{G}$
26	1 25	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
27	4 26	syl	$⊢ F \in (G GrpHom H) \to 0_{G} \in X$
28		fveq2	$⊢ x = 0_{G} \to F (x) = F (0_{G})$
29	28	fveq1d	$⊢ x = 0_{G} \to F (x) (y) = F (0_{G}) (y)$
30		fveq2	$⊢ y = z \to F (0_{G}) (y) = F (0_{G}) (z)$
31		fvex	$⊢ F (0_{G}) (z) \in V$
32	29 30 3 31	ovmpo	$⊢ (0_{G} \in X \land z \in Y) \to 0_{G} \underset{˙}{\oplus} z = F (0_{G}) (z)$
33	27 32	sylan	$⊢ (F \in (G GrpHom H) \land z \in Y) \to 0_{G} \underset{˙}{\oplus} z = F (0_{G}) (z)$
34		eqid	$⊢ 0_{H} = 0_{H}$
35	25 34	ghmid	$⊢ F \in (G GrpHom H) \to F (0_{G}) = 0_{H}$
36	35	adantr	$⊢ (F \in (G GrpHom H) \land z \in Y) \to F (0_{G}) = 0_{H}$
37	10	adantr	$⊢ (F \in (G GrpHom H) \land z \in Y) \to Y \in V$
38	2	symgid	$⊢ Y \in V \to {I ↾}_{Y} = 0_{H}$
39	37 38	syl	$⊢ (F \in (G GrpHom H) \land z \in Y) \to {I ↾}_{Y} = 0_{H}$
40	36 39	eqtr4d	$⊢ (F \in (G GrpHom H) \land z \in Y) \to F (0_{G}) = {I ↾}_{Y}$
41	40	fveq1d	$⊢ (F \in (G GrpHom H) \land z \in Y) \to F (0_{G}) (z) = ({I ↾}_{Y}) (z)$
42		fvresi	$⊢ z \in Y \to ({I ↾}_{Y}) (z) = z$
43	42	adantl	$⊢ (F \in (G GrpHom H) \land z \in Y) \to ({I ↾}_{Y}) (z) = z$
44	33 41 43	3eqtrd	$⊢ (F \in (G GrpHom H) \land z \in Y) \to 0_{G} \underset{˙}{\oplus} z = z$
45	12	ad2antrr	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F : X ⟶ {Base}_{H}$
46		simprr	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to v \in X$
47	45 46	ffvelcdmd	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (v) \in {Base}_{H}$
48	10	ad2antrr	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to Y \in V$
49	2 11	elsymgbas	$⊢ Y \in V \to (F (v) \in {Base}_{H} \leftrightarrow F (v) : Y \underset{1-1 onto}{⟶} Y)$
50	48 49	syl	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to (F (v) \in {Base}_{H} \leftrightarrow F (v) : Y \underset{1-1 onto}{⟶} Y)$
51	47 50	mpbid	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (v) : Y \underset{1-1 onto}{⟶} Y$
52		f1of	$⊢ F (v) : Y \underset{1-1 onto}{⟶} Y \to F (v) : Y ⟶ Y$
53	51 52	syl	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (v) : Y ⟶ Y$
54		simplr	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to z \in Y$
55		fvco3	$⊢ (F (v) : Y ⟶ Y \land z \in Y) \to (F (u) \circ F (v)) (z) = F (u) (F (v) (z))$
56	53 54 55	syl2anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to (F (u) \circ F (v)) (z) = F (u) (F (v) (z))$
57		simpll	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F \in (G GrpHom H)$
58		simprl	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to u \in X$
59		eqid	$⊢ +_{G} = +_{G}$
60		eqid	$⊢ +_{H} = +_{H}$
61	1 59 60	ghmlin	$⊢ (F \in (G GrpHom H) \land u \in X \land v \in X) \to F (u +_{G} v) = F (u) +_{H} F (v)$
62	57 58 46 61	syl3anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (u +_{G} v) = F (u) +_{H} F (v)$
63	45 58	ffvelcdmd	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (u) \in {Base}_{H}$
64	2 11 60	symgov	$⊢ (F (u) \in {Base}_{H} \land F (v) \in {Base}_{H}) \to F (u) +_{H} F (v) = F (u) \circ F (v)$
65	63 47 64	syl2anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (u) +_{H} F (v) = F (u) \circ F (v)$
66	62 65	eqtrd	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (u +_{G} v) = F (u) \circ F (v)$
67	66	fveq1d	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (u +_{G} v) (z) = (F (u) \circ F (v)) (z)$
68	53 54	ffvelcdmd	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (v) (z) \in Y$
69		fveq2	$⊢ x = u \to F (x) = F (u)$
70	69	fveq1d	$⊢ x = u \to F (x) (y) = F (u) (y)$
71		fveq2	$⊢ y = F (v) (z) \to F (u) (y) = F (u) (F (v) (z))$
72		fvex	$⊢ F (u) (F (v) (z)) \in V$
73	70 71 3 72	ovmpo	$⊢ (u \in X \land F (v) (z) \in Y) \to u \underset{˙}{\oplus} F (v) (z) = F (u) (F (v) (z))$
74	58 68 73	syl2anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to u \underset{˙}{\oplus} F (v) (z) = F (u) (F (v) (z))$
75	56 67 74	3eqtr4d	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to F (u +_{G} v) (z) = u \underset{˙}{\oplus} F (v) (z)$
76	4	ad2antrr	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to G \in Grp$
77	1 59	grpcl	$⊢ (G \in Grp \land u \in X \land v \in X) \to u +_{G} v \in X$
78	76 58 46 77	syl3anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to u +_{G} v \in X$
79		fveq2	$⊢ x = u +_{G} v \to F (x) = F (u +_{G} v)$
80	79	fveq1d	$⊢ x = u +_{G} v \to F (x) (y) = F (u +_{G} v) (y)$
81		fveq2	$⊢ y = z \to F (u +_{G} v) (y) = F (u +_{G} v) (z)$
82		fvex	$⊢ F (u +_{G} v) (z) \in V$
83	80 81 3 82	ovmpo	$⊢ (u +_{G} v \in X \land z \in Y) \to (u +_{G} v) \underset{˙}{\oplus} z = F (u +_{G} v) (z)$
84	78 54 83	syl2anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to (u +_{G} v) \underset{˙}{\oplus} z = F (u +_{G} v) (z)$
85		fveq2	$⊢ x = v \to F (x) = F (v)$
86	85	fveq1d	$⊢ x = v \to F (x) (y) = F (v) (y)$
87		fveq2	$⊢ y = z \to F (v) (y) = F (v) (z)$
88		fvex	$⊢ F (v) (z) \in V$
89	86 87 3 88	ovmpo	$⊢ (v \in X \land z \in Y) \to v \underset{˙}{\oplus} z = F (v) (z)$
90	46 54 89	syl2anc	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to v \underset{˙}{\oplus} z = F (v) (z)$
91	90	oveq2d	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z) = u \underset{˙}{\oplus} F (v) (z)$
92	75 84 91	3eqtr4d	$⊢ ((F \in (G GrpHom H) \land z \in Y) \land (u \in X \land v \in X)) \to (u +_{G} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z)$
93	92	ralrimivva	$⊢ (F \in (G GrpHom H) \land z \in Y) \to \forall u \in X \forall v \in X (u +_{G} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z)$
94	44 93	jca	$⊢ (F \in (G GrpHom H) \land z \in Y) \to (0_{G} \underset{˙}{\oplus} z = z \land \forall u \in X \forall v \in X (u +_{G} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z))$
95	94	ralrimiva	$⊢ F \in (G GrpHom H) \to \forall z \in Y (0_{G} \underset{˙}{\oplus} z = z \land \forall u \in X \forall v \in X (u +_{G} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z))$
96	24 95	jca	$⊢ F \in (G GrpHom H) \to (\underset{˙}{\oplus} : X \times Y ⟶ Y \land \forall z \in Y (0_{G} \underset{˙}{\oplus} z = z \land \forall u \in X \forall v \in X (u +_{G} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z)))$
97	1 59 25	isga	$⊢ \underset{˙}{\oplus} \in (G GrpAct Y) \leftrightarrow ((G \in Grp \land Y \in V) \land (\underset{˙}{\oplus} : X \times Y ⟶ Y \land \forall z \in Y (0_{G} \underset{˙}{\oplus} z = z \land \forall u \in X \forall v \in X (u +_{G} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z))))$
98	4 10 96 97	syl21anbrc	$⊢ F \in (G GrpHom H) \to \underset{˙}{\oplus} \in (G GrpAct Y)$

Metamath Proof Explorer

Theorem lactghmga

Proof