Metamath Proof Explorer

Theorem isghm

Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014) (Proof shortened by SN, 5-Jun-2025)

Ref Expression
Hypotheses isghm.w ⊢ 𝑋 = ( Base ‘ 𝑆 )
isghm.x ⊢ 𝑌 = ( Base ‘ 𝑇 )
isghm.a ⊢ + = ( +g ‘ 𝑆 )
isghm.b ⊢ ⨣ = ( +g ‘ 𝑇 )
Assertion isghm ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isghm.w ⊢ 𝑋 = ( Base ‘ 𝑆 )
2 isghm.x ⊢ 𝑌 = ( Base ‘ 𝑇 )
3 isghm.a ⊢ + = ( +g ‘ 𝑆 )
4 isghm.b ⊢ ⨣ = ( +g ‘ 𝑇 )
5 df-ghm ⊢ GrpHom = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } )
6 5 elmpocl ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) )
7 fvex ⊢ ( Base ‘ 𝑠 ) ∈ V
8 feq2 ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ) )
9 raleq ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
10 9 raleqbi1dv ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
11 8 10 anbi12d ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ) )
12 7 11 sbcie ⊢ ( [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
13 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
14 13 1 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝑋 )
15 14 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = 𝑋 )
16 fveq2 ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = ( Base ‘ 𝑇 ) )
17 16 2 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝑌 )
18 17 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑡 ) = 𝑌 )
19 15 18 feq23d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
20 fveq2 ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ( +g ‘ 𝑆 ) )
21 20 3 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = + )
22 21 oveqd ⊢ ( 𝑠 = 𝑆 → ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) = ( 𝑢 + 𝑣 ) )
23 22 fveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) )
24 fveq2 ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ( +g ‘ 𝑇 ) )
25 24 4 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ⨣ )
26 25 oveqd ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) )
27 23 26 eqeqan12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
28 15 27 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
29 15 28 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
30 19 29 anbi12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ) )
31 12 30 bitrid ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ) )
32 31 abbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } )
33 2 fvexi ⊢ 𝑌 ∈ V
34 fsetex ⊢ ( 𝑌 ∈ V → { 𝑓 ∣ 𝑓 : 𝑋 ⟶ 𝑌 } ∈ V )
35 33 34 ax-mp ⊢ { 𝑓 ∣ 𝑓 : 𝑋 ⟶ 𝑌 } ∈ V
36 abanssl ⊢ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : 𝑋 ⟶ 𝑌 }
37 35 36 ssexi ⊢ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ∈ V
38 32 5 37 ovmpoa ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } )
39 38 eleq2d ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ) )
40 1 fvexi ⊢ 𝑋 ∈ V
41 fex2 ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝐹 ∈ V )
42 40 33 41 mp3an23 ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 ∈ V )
43 42 adantr ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) → 𝐹 ∈ V )
44 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋 ⟶ 𝑌 ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
45 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) )
46 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
47 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
48 46 47 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) )
49 45 48 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
50 49 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
51 44 50 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
52 43 51 elab3 ⊢ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
53 39 52 bitrdi ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
54 6 53 biadanii ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )