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

Metamath Proof Explorer

Definition df-ghomOLD

Description: Obsolete version of df-ghm as of 15-Mar-2020. Define the set of group homomorphisms from g to h . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

Ref Expression
Assertion df-ghomOLD GrpOpHom = ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cghomOLD ⊢ GrpOpHom
1 vg ⊢ 𝑔
2 cgr ⊢ GrpOp
3 vh ⊢ ℎ
4 vf ⊢ 𝑓
5 4 cv ⊢ 𝑓
6 1 cv ⊢ 𝑔
7 6 crn ⊢ ran 𝑔
8 3 cv ⊢ ℎ
9 8 crn ⊢ ran ℎ
10 7 9 5 wf ⊢ 𝑓 : ran 𝑔 ⟶ ran ℎ
11 vx ⊢ 𝑥
12 vy ⊢ 𝑦
13 11 cv ⊢ 𝑥
14 13 5 cfv ⊢ ( 𝑓 ‘ 𝑥 )
15 12 cv ⊢ 𝑦
16 15 5 cfv ⊢ ( 𝑓 ‘ 𝑦 )
17 14 16 8 co ⊢ ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) )
18 13 15 6 co ⊢ ( 𝑥 𝑔 𝑦 )
19 18 5 cfv ⊢ ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
20 17 19 wceq ⊢ ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
21 20 12 7 wral ⊢ ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
22 21 11 7 wral ⊢ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) )
23 10 22 wa ⊢ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) )
24 23 4 cab ⊢ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) }
25 1 3 2 2 24 cmpo ⊢ ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )
26 0 25 wceq ⊢ GrpOpHom = ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )