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

Metamath Proof Explorer

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 𝐻 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝐻 ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) )