conjga

Description: Group conjugation induces a group action. (Contributed by Thierry Arnoux, 18-Nov-2025)

	Ref	Expression
Hypotheses	cntrval2.1	$⊢ B = {Base}_{M}$
	cntrval2.2	$⊢ \underset{˙}{+} = +_{M}$
	cntrval2.3	$⊢ \underset{˙}{-} = -_{M}$
	cntrval2.4	$⊢ \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
Assertion	conjga	$⊢ M \in Grp \to \underset{˙}{\oplus} \in (M GrpAct B)$

Proof

Step	Hyp	Ref	Expression
1		cntrval2.1	$⊢ B = {Base}_{M}$
2		cntrval2.2	$⊢ \underset{˙}{+} = +_{M}$
3		cntrval2.3	$⊢ \underset{˙}{-} = -_{M}$
4		cntrval2.4	$⊢ \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
5		id	$⊢ M \in Grp \to M \in Grp$
6	1	fvexi	$⊢ B \in V$
7	6	a1i	$⊢ M \in Grp \to B \in V$
8	5	adantr	$⊢ (M \in Grp \land z \in (B \times B)) \to M \in Grp$
9		xp1st	$⊢ z \in (B \times B) \to 1^{st} (z) \in B$
10	9	adantl	$⊢ (M \in Grp \land z \in (B \times B)) \to 1^{st} (z) \in B$
11		xp2nd	$⊢ z \in (B \times B) \to 2^{nd} (z) \in B$
12	11	adantl	$⊢ (M \in Grp \land z \in (B \times B)) \to 2^{nd} (z) \in B$
13	1 2 8 10 12	grpcld	$⊢ (M \in Grp \land z \in (B \times B)) \to 1^{st} (z) \underset{˙}{+} 2^{nd} (z) \in B$
14	1 3 8 13 10	grpsubcld	$⊢ (M \in Grp \land z \in (B \times B)) \to (1^{st} (z) \underset{˙}{+} 2^{nd} (z)) \underset{˙}{-} 1^{st} (z) \in B$
15		vex	$⊢ x \in V$
16		vex	$⊢ y \in V$
17	15 16	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
18	15 16	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
19	17 18	oveq12d	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) \underset{˙}{+} 2^{nd} (z) = x \underset{˙}{+} y$
20	19 17	oveq12d	$⊢ z = ⟨x, y⟩ \to (1^{st} (z) \underset{˙}{+} 2^{nd} (z)) \underset{˙}{-} 1^{st} (z) = (x \underset{˙}{+} y) \underset{˙}{-} x$
21	20	mpompt	$⊢ (z \in (B \times B) ⟼ (1^{st} (z) \underset{˙}{+} 2^{nd} (z)) \underset{˙}{-} 1^{st} (z)) = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
22	4 21	eqtr4i	$⊢ \underset{˙}{\oplus} = (z \in (B \times B) ⟼ (1^{st} (z) \underset{˙}{+} 2^{nd} (z)) \underset{˙}{-} 1^{st} (z))$
23	14 22	fmptd	$⊢ M \in Grp \to \underset{˙}{\oplus} : B \times B ⟶ B$
24	4	a1i	$⊢ (M \in Grp \land z \in B) \to \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
25		simplr	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to x = 0_{M}$
26		simpr	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to y = z$
27	25 26	oveq12d	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to x \underset{˙}{+} y = 0_{M} \underset{˙}{+} z$
28	27 25	oveq12d	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to (x \underset{˙}{+} y) \underset{˙}{-} x = (0_{M} \underset{˙}{+} z) \underset{˙}{-} 0_{M}$
29	5	ad3antrrr	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to M \in Grp$
30		eqid	$⊢ 0_{M} = 0_{M}$
31	1 30	grpidcl	$⊢ M \in Grp \to 0_{M} \in B$
32	31	ad3antrrr	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to 0_{M} \in B$
33		simpllr	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to z \in B$
34	1 2 29 32 33	grpcld	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to 0_{M} \underset{˙}{+} z \in B$
35	1 30 3	grpsubid1	$⊢ (M \in Grp \land 0_{M} \underset{˙}{+} z \in B) \to (0_{M} \underset{˙}{+} z) \underset{˙}{-} 0_{M} = 0_{M} \underset{˙}{+} z$
36	29 34 35	syl2anc	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to (0_{M} \underset{˙}{+} z) \underset{˙}{-} 0_{M} = 0_{M} \underset{˙}{+} z$
37	1 2 30 29 33	grplidd	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to 0_{M} \underset{˙}{+} z = z$
38	28 36 37	3eqtrd	$⊢ (((M \in Grp \land z \in B) \land x = 0_{M}) \land y = z) \to (x \underset{˙}{+} y) \underset{˙}{-} x = z$
39	38	anasss	$⊢ ((M \in Grp \land z \in B) \land (x = 0_{M} \land y = z)) \to (x \underset{˙}{+} y) \underset{˙}{-} x = z$
40	31	adantr	$⊢ (M \in Grp \land z \in B) \to 0_{M} \in B$
41		simpr	$⊢ (M \in Grp \land z \in B) \to z \in B$
42	24 39 40 41 41	ovmpod	$⊢ (M \in Grp \land z \in B) \to 0_{M} \underset{˙}{\oplus} z = z$
43	5	ad3antrrr	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to M \in Grp$
44		simplr	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to u \in B$
45		simpr	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to v \in B$
46		simpllr	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to z \in B$
47	1 2 43 44 45 46	grpassd	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to (u \underset{˙}{+} v) \underset{˙}{+} z = u \underset{˙}{+} (v \underset{˙}{+} z)$
48	47	oveq1d	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to ((u \underset{˙}{+} v) \underset{˙}{+} z) \underset{˙}{-} (u \underset{˙}{+} v) = (u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} (u \underset{˙}{+} v)$
49	1 2 43 45 46	grpcld	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to v \underset{˙}{+} z \in B$
50	1 2 43 44 49	grpcld	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to u \underset{˙}{+} (v \underset{˙}{+} z) \in B$
51	1 2 3	grpsubsub4	$⊢ (M \in Grp \land (u \underset{˙}{+} (v \underset{˙}{+} z) \in B \land v \in B \land u \in B)) \to ((u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} v) \underset{˙}{-} u = (u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} (u \underset{˙}{+} v)$
52	43 50 45 44 51	syl13anc	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to ((u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} v) \underset{˙}{-} u = (u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} (u \underset{˙}{+} v)$
53	1 2 3	grpaddsubass	$⊢ (M \in Grp \land (u \in B \land v \underset{˙}{+} z \in B \land v \in B)) \to (u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} v = u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)$
54	43 44 49 45 53	syl13anc	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to (u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} v = u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)$
55	54	oveq1d	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to ((u \underset{˙}{+} (v \underset{˙}{+} z)) \underset{˙}{-} v) \underset{˙}{-} u = (u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)) \underset{˙}{-} u$
56	48 52 55	3eqtr2d	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to ((u \underset{˙}{+} v) \underset{˙}{+} z) \underset{˙}{-} (u \underset{˙}{+} v) = (u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)) \underset{˙}{-} u$
57	4	a1i	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to \underset{˙}{\oplus} = (x \in B, y \in B ⟼ (x \underset{˙}{+} y) \underset{˙}{-} x)$
58		simprl	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \underset{˙}{+} v \land y = z)) \to x = u \underset{˙}{+} v$
59		simprr	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \underset{˙}{+} v \land y = z)) \to y = z$
60	58 59	oveq12d	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \underset{˙}{+} v \land y = z)) \to x \underset{˙}{+} y = (u \underset{˙}{+} v) \underset{˙}{+} z$
61	60 58	oveq12d	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \underset{˙}{+} v \land y = z)) \to (x \underset{˙}{+} y) \underset{˙}{-} x = ((u \underset{˙}{+} v) \underset{˙}{+} z) \underset{˙}{-} (u \underset{˙}{+} v)$
62	1 2 43 44 45	grpcld	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to u \underset{˙}{+} v \in B$
63		ovexd	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to ((u \underset{˙}{+} v) \underset{˙}{+} z) \underset{˙}{-} (u \underset{˙}{+} v) \in V$
64	57 61 62 46 63	ovmpod	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to (u \underset{˙}{+} v) \underset{˙}{\oplus} z = ((u \underset{˙}{+} v) \underset{˙}{+} z) \underset{˙}{-} (u \underset{˙}{+} v)$
65		simprl	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \land y = v \underset{˙}{\oplus} z)) \to x = u$
66		simprr	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \land y = v \underset{˙}{\oplus} z)) \to y = v \underset{˙}{\oplus} z$
67		simprl	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = v \land y = z)) \to x = v$
68		simprr	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = v \land y = z)) \to y = z$
69	67 68	oveq12d	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = v \land y = z)) \to x \underset{˙}{+} y = v \underset{˙}{+} z$
70	69 67	oveq12d	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = v \land y = z)) \to (x \underset{˙}{+} y) \underset{˙}{-} x = (v \underset{˙}{+} z) \underset{˙}{-} v$
71		ovexd	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to (v \underset{˙}{+} z) \underset{˙}{-} v \in V$
72	57 70 45 46 71	ovmpod	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to v \underset{˙}{\oplus} z = (v \underset{˙}{+} z) \underset{˙}{-} v$
73	72	adantr	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \land y = v \underset{˙}{\oplus} z)) \to v \underset{˙}{\oplus} z = (v \underset{˙}{+} z) \underset{˙}{-} v$
74	66 73	eqtrd	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \land y = v \underset{˙}{\oplus} z)) \to y = (v \underset{˙}{+} z) \underset{˙}{-} v$
75	65 74	oveq12d	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \land y = v \underset{˙}{\oplus} z)) \to x \underset{˙}{+} y = u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)$
76	75 65	oveq12d	$⊢ ((((M \in Grp \land z \in B) \land u \in B) \land v \in B) \land (x = u \land y = v \underset{˙}{\oplus} z)) \to (x \underset{˙}{+} y) \underset{˙}{-} x = (u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)) \underset{˙}{-} u$
77	23	ad3antrrr	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to \underset{˙}{\oplus} : B \times B ⟶ B$
78	77 45 46	fovcdmd	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to v \underset{˙}{\oplus} z \in B$
79		ovexd	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to (u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)) \underset{˙}{-} u \in V$
80	57 76 44 78 79	ovmpod	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z) = (u \underset{˙}{+} ((v \underset{˙}{+} z) \underset{˙}{-} v)) \underset{˙}{-} u$
81	56 64 80	3eqtr4d	$⊢ (((M \in Grp \land z \in B) \land u \in B) \land v \in B) \to (u \underset{˙}{+} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z)$
82	81	anasss	$⊢ ((M \in Grp \land z \in B) \land (u \in B \land v \in B)) \to (u \underset{˙}{+} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z)$
83	82	ralrimivva	$⊢ (M \in Grp \land z \in B) \to \forall u \in B \forall v \in B (u \underset{˙}{+} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z)$
84	42 83	jca	$⊢ (M \in Grp \land z \in B) \to (0_{M} \underset{˙}{\oplus} z = z \land \forall u \in B \forall v \in B (u \underset{˙}{+} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z))$
85	84	ralrimiva	$⊢ M \in Grp \to \forall z \in B (0_{M} \underset{˙}{\oplus} z = z \land \forall u \in B \forall v \in B (u \underset{˙}{+} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z))$
86	1 2 30	isga	$⊢ \underset{˙}{\oplus} \in (M GrpAct B) \leftrightarrow ((M \in Grp \land B \in V) \land (\underset{˙}{\oplus} : B \times B ⟶ B \land \forall z \in B (0_{M} \underset{˙}{\oplus} z = z \land \forall u \in B \forall v \in B (u \underset{˙}{+} v) \underset{˙}{\oplus} z = u \underset{˙}{\oplus} (v \underset{˙}{\oplus} z))))$
87	5 7 23 85 86	syl22anbrc	$⊢ M \in Grp \to \underset{˙}{\oplus} \in (M GrpAct B)$

Metamath Proof Explorer

Theorem conjga

Proof