Theorem ghomlinOLD

Description: Obsolete version of ghmlin as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	ghomlinOLD.1	⊢ 𝑋 = ran 𝐺
Assertion	ghomlinOLD	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ghomlinOLD.1	⊢ 𝑋 = ran 𝐺
2		eqid	⊢ ran 𝐻 = ran 𝐻
3	1 2	elghomOLD	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : 𝑋 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
4	3	biimp3a	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 : 𝑋 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
5	4	simprd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
6		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
7	6	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) )
8		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑦 ) = ( 𝐴 𝐺 𝑦 ) )
9	8	fveq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) )
10	7 9	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) ) )
11		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
12	11	oveq2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) )
13		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
14	13	fveq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) )
15	12 14	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) ) )
16	10 15	rspc2v	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) ) )
17	5 16	mpan9	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) )