This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` M )
cntrval2.3 
|- .- = ( -g ` M )
cntrval2.4 
|- .(+) = ( x e. B , y e. B |-> ( ( x .+ y ) .- x ) )
Assertion conjga 
|- ( M e. Grp -> .(+) e. ( M GrpAct B ) )

Proof

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