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

Metamath Proof Explorer

Theorem elghomlem1OLD

Description: Obsolete as of 15-Mar-2020. Lemma for elghomOLD . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis elghomlem1OLD.1 ⊢ 𝑆 = { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) }
Assertion elghomlem1OLD ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐺 GrpOpHom 𝐻 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 elghomlem1OLD.1 ⊢ 𝑆 = { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) }
2 rnexg ⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
3 rnexg ⊢ ( 𝐻 ∈ GrpOp → ran 𝐻 ∈ V )
4 1 fabexg ⊢ ( ( ran 𝐺 ∈ V ∧ ran 𝐻 ∈ V ) → 𝑆 ∈ V )
5 2 3 4 syl2an ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → 𝑆 ∈ V )
6 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
7 6 feq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑓 : ran 𝑔 ⟶ ran ℎ ↔ 𝑓 : ran 𝐺 ⟶ ran ℎ ) )
8 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
9 8 fveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) )
10 9 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
11 6 10 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ↔ ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
12 6 11 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
13 7 12 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) ↔ ( 𝑓 : ran 𝐺 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
14 13 abbidv ⊢ ( 𝑔 = 𝐺 → { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) } )
15 rneq ⊢ ( ℎ = 𝐻 → ran ℎ = ran 𝐻 )
16 15 feq3d ⊢ ( ℎ = 𝐻 → ( 𝑓 : ran 𝐺 ⟶ ran ℎ ↔ 𝑓 : ran 𝐺 ⟶ ran 𝐻 ) )
17 oveq ⊢ ( ℎ = 𝐻 → ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) )
18 17 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
19 18 2ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
20 16 19 anbi12d ⊢ ( ℎ = 𝐻 → ( ( 𝑓 : ran 𝐺 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ↔ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
21 20 abbidv ⊢ ( ℎ = 𝐻 → { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) 𝐻 ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) } )
22 21 1 eqtr4di ⊢ ( ℎ = 𝐻 → { 𝑓 ∣ ( 𝑓 : ran 𝐺 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) ) } = 𝑆 )
23 df-ghomOLD ⊢ GrpOpHom = ( 𝑔 ∈ GrpOp , ℎ ∈ GrpOp ↦ { 𝑓 ∣ ( 𝑓 : ran 𝑔 ⟶ ran ℎ ∧ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑓 ‘ 𝑥 ) ℎ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 𝑔 𝑦 ) ) ) } )
24 14 22 23 ovmpog ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝑆 ∈ V ) → ( 𝐺 GrpOpHom 𝐻 ) = 𝑆 )
25 5 24 mpd3an3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐺 GrpOpHom 𝐻 ) = 𝑆 )