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 𝐻 ) = 𝑆 )