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

Metamath Proof Explorer

Theorem elghomOLD

Description: Obsolete version of isghm as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H . (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses elghomOLD.1 ⊢ 𝑋 = ran 𝐺
elghomOLD.2 ⊢ 𝑊 = ran 𝐻
Assertion elghomOLD ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elghomOLD.1 ⊢ 𝑋 = ran 𝐺
2 elghomOLD.2 ⊢ 𝑊 = ran 𝐻
3 eqid ⊢ { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) }
4 3 elghomlem2OLD ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
5 1 2 feq23i ⊢ ( 𝐹 : 𝑋 ⟶ 𝑊 ↔ 𝐹 : ran 𝐺 ⟶ ran 𝐻 )
6 1 raleqi ⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
7 1 6 raleqbii ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
8 5 7 anbi12i ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
9 4 8 bitr4di ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )