Metamath Proof Explorer

Theorem ghomidOLD

Description: Obsolete version of ghmid as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ghomidOLD.1 ⊢ 𝑈 = ( GId ‘ 𝐺 )
ghomidOLD.2 ⊢ 𝑇 = ( GId ‘ 𝐻 )
Assertion ghomidOLD ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 ‘ 𝑈 ) = 𝑇 )

Proof

Step Hyp Ref Expression
1 ghomidOLD.1 ⊢ 𝑈 = ( GId ‘ 𝐺 )
2 ghomidOLD.2 ⊢ 𝑇 = ( GId ‘ 𝐻 )
3 eqid ⊢ ran 𝐺 = ran 𝐺
4 3 1 grpoidcl ⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ ran 𝐺 )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝑈 ∈ ran 𝐺 )
6 5 5 jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝑈 ∈ ran 𝐺 ∧ 𝑈 ∈ ran 𝐺 ) )
7 3 ghomlinOLD ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑈 ∈ ran 𝐺 ∧ 𝑈 ∈ ran 𝐺 ) ) → ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ ( 𝑈 𝐺 𝑈 ) ) )
8 6 7 mpdan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ ( 𝑈 𝐺 𝑈 ) ) )
9 3 1 grpolid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑈 ∈ ran 𝐺 ) → ( 𝑈 𝐺 𝑈 ) = 𝑈 )
10 4 9 mpdan ⊢ ( 𝐺 ∈ GrpOp → ( 𝑈 𝐺 𝑈 ) = 𝑈 )
11 10 fveq2d ⊢ ( 𝐺 ∈ GrpOp → ( 𝐹 ‘ ( 𝑈 𝐺 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) )
12 11 3ad2ant1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 ‘ ( 𝑈 𝐺 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) )
13 8 12 eqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) )
14 eqid ⊢ ran 𝐻 = ran 𝐻
15 3 14 elghomOLD ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
16 15 biimp3a ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐻 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
17 16 simpld ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 : ran 𝐺 ⟶ ran 𝐻 )
18 17 5 ffvelcdmd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ran 𝐻 )
19 14 2 grpoid ⊢ ( ( 𝐻 ∈ GrpOp ∧ ( 𝐹 ‘ 𝑈 ) ∈ ran 𝐻 ) → ( ( 𝐹 ‘ 𝑈 ) = 𝑇 ↔ ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) ) )
20 19 ex ⊢ ( 𝐻 ∈ GrpOp → ( ( 𝐹 ‘ 𝑈 ) ∈ ran 𝐻 → ( ( 𝐹 ‘ 𝑈 ) = 𝑇 ↔ ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) ) ) )
21 20 3ad2ant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( ( 𝐹 ‘ 𝑈 ) ∈ ran 𝐻 → ( ( 𝐹 ‘ 𝑈 ) = 𝑇 ↔ ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) ) ) )
22 18 21 mpd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( ( 𝐹 ‘ 𝑈 ) = 𝑇 ↔ ( ( 𝐹 ‘ 𝑈 ) 𝐻 ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) ) )
23 13 22 mpbird ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 ‘ 𝑈 ) = 𝑇 )