Metamath Proof Explorer


Theorem isghm

Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014)

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 feq2d ( 𝑠 = 𝑆 → ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ) )
16 fveq2 ( 𝑠 = 𝑆 → ( +g𝑠 ) = ( +g𝑆 ) )
17 16 3 eqtr4di ( 𝑠 = 𝑆 → ( +g𝑠 ) = + )
18 17 oveqd ( 𝑠 = 𝑆 → ( 𝑢 ( +g𝑠 ) 𝑣 ) = ( 𝑢 + 𝑣 ) )
19 18 fveqeq2d ( 𝑠 = 𝑆 → ( ( 𝑓 ‘ ( 𝑢 ( +g𝑠 ) 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ↔ ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) )
20 14 19 raleqbidv ( 𝑠 = 𝑆 → ( ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g𝑠 ) 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ↔ ∀ 𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) )
21 14 20 raleqbidv ( 𝑠 = 𝑆 → ( ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g𝑠 ) 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ↔ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) )
22 15 21 anbi12d ( 𝑠 = 𝑆 → ( ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g𝑠 ) 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) ) )
23 12 22 syl5bb ( 𝑠 = 𝑆 → ( [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑤𝑣𝑤 ( 𝑓 ‘ ( 𝑢 ( +g𝑠 ) 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) ) )
24 23 abbidv ( 𝑠 = 𝑆 → { 𝑓[ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑤𝑣𝑤 ( 𝑓 ‘ ( 𝑢 ( +g𝑠 ) 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) } )
25 fveq2 ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = ( Base ‘ 𝑇 ) )
26 25 2 eqtr4di ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝑌 )
27 26 feq3d ( 𝑡 = 𝑇 → ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : 𝑋𝑌 ) )
28 fveq2 ( 𝑡 = 𝑇 → ( +g𝑡 ) = ( +g𝑇 ) )
29 28 4 eqtr4di ( 𝑡 = 𝑇 → ( +g𝑡 ) = )
30 29 oveqd ( 𝑡 = 𝑇 → ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) )
31 30 eqeq2d ( 𝑡 = 𝑇 → ( ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ↔ ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) )
32 31 2ralbidv ( 𝑡 = 𝑇 → ( ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ↔ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) )
33 27 32 anbi12d ( 𝑡 = 𝑇 → ( ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) ↔ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) ) )
34 33 abbidv ( 𝑡 = 𝑇 → { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( +g𝑡 ) ( 𝑓𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) } )
35 1 fvexi 𝑋 ∈ V
36 2 fvexi 𝑌 ∈ V
37 mapex ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { 𝑓𝑓 : 𝑋𝑌 } ∈ V )
38 35 36 37 mp2an { 𝑓𝑓 : 𝑋𝑌 } ∈ V
39 simpl ( ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) → 𝑓 : 𝑋𝑌 )
40 39 ss2abi { 𝑓 ∣ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) } ⊆ { 𝑓𝑓 : 𝑋𝑌 }
41 38 40 ssexi { 𝑓 ∣ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) } ∈ V
42 24 34 5 41 ovmpo ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = { 𝑓 ∣ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) } )
43 42 eleq2d ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) } ) )
44 fex ( ( 𝐹 : 𝑋𝑌𝑋 ∈ V ) → 𝐹 ∈ V )
45 35 44 mpan2 ( 𝐹 : 𝑋𝑌𝐹 ∈ V )
46 45 adantr ( ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) → 𝐹 ∈ V )
47 feq1 ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋𝑌𝐹 : 𝑋𝑌 ) )
48 fveq1 ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) )
49 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑢 ) = ( 𝐹𝑢 ) )
50 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑣 ) = ( 𝐹𝑣 ) )
51 49 50 oveq12d ( 𝑓 = 𝐹 → ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) )
52 48 51 eqeq12d ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ↔ ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) )
53 52 2ralbidv ( 𝑓 = 𝐹 → ( ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ↔ ∀ 𝑢𝑋𝑣𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) )
54 47 53 anbi12d ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) ) )
55 46 54 elab3 ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓𝑢 ) ( 𝑓𝑣 ) ) ) } ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) )
56 43 55 bitrdi ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) ) )
57 6 56 biadanii ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑢𝑋𝑣𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹𝑢 ) ( 𝐹𝑣 ) ) ) ) )