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 ⊢ S = f | f : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y
Assertion elghomlem1OLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → G GrpOpHom H = S

Proof

Step Hyp Ref Expression
1 elghomlem1OLD.1 ⊢ S = f | f : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y
2 rnexg ⊢ G ∈ GrpOp → ran ⁡ G ∈ V
3 rnexg ⊢ H ∈ GrpOp → ran ⁡ H ∈ V
4 1 fabexg ⊢ ran ⁡ G ∈ V ∧ ran ⁡ H ∈ V → S ∈ V
5 2 3 4 syl2an ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → S ∈ V
6 rneq ⊢ g = G → ran ⁡ g = ran ⁡ G
7 6 feq2d ⊢ g = G → f : ran ⁡ g ⟶ ran ⁡ h ↔ f : ran ⁡ G ⟶ ran ⁡ h
8 oveq ⊢ g = G → x g y = x G y
9 8 fveq2d ⊢ g = G → f ⁡ x g y = f ⁡ x G y
10 9 eqeq2d ⊢ g = G → f ⁡ x h f ⁡ y = f ⁡ x g y ↔ f ⁡ x h f ⁡ y = f ⁡ x G y
11 6 10 raleqbidv ⊢ g = G → ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y ↔ ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y
12 6 11 raleqbidv ⊢ g = G → ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y ↔ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y
13 7 12 anbi12d ⊢ g = G → f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y ↔ f : ran ⁡ G ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y
14 13 abbidv ⊢ g = G → f | f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y = f | f : ran ⁡ G ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y
15 rneq ⊢ h = H → ran ⁡ h = ran ⁡ H
16 15 feq3d ⊢ h = H → f : ran ⁡ G ⟶ ran ⁡ h ↔ f : ran ⁡ G ⟶ ran ⁡ H
17 oveq ⊢ h = H → f ⁡ x h f ⁡ y = f ⁡ x H f ⁡ y
18 17 eqeq1d ⊢ h = H → f ⁡ x h f ⁡ y = f ⁡ x G y ↔ f ⁡ x H f ⁡ y = f ⁡ x G y
19 18 2ralbidv ⊢ h = H → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y ↔ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y
20 16 19 anbi12d ⊢ h = H → f : ran ⁡ G ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y ↔ f : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y
21 20 abbidv ⊢ h = H → f | f : ran ⁡ G ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y = f | f : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y
22 21 1 eqtr4di ⊢ h = H → f | f : ran ⁡ G ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x h f ⁡ y = f ⁡ x G y = S
23 df-ghomOLD ⊢ GrpOpHom = g ∈ GrpOp , h ∈ GrpOp ⟼ f | f : ran ⁡ g ⟶ ran ⁡ h ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g f ⁡ x h f ⁡ y = f ⁡ x g y
24 14 22 23 ovmpog ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ S ∈ V → G GrpOpHom H = S
25 5 24 mpd3an3 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → G GrpOpHom H = S