Metamath Proof Explorer

Theorem elghomlem2OLD

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 elghomlem2OLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ G GrpOpHom H ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y

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 1 elghomlem1OLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → G GrpOpHom H = S
3 2 eleq2d ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ G GrpOpHom H ↔ F ∈ S
4 elex ⊢ F ∈ S → F ∈ V
5 feq1 ⊢ f = F → f : ran ⁡ G ⟶ ran ⁡ H ↔ F : ran ⁡ G ⟶ ran ⁡ H
6 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
7 fveq1 ⊢ f = F → f ⁡ y = F ⁡ y
8 6 7 oveq12d ⊢ f = F → f ⁡ x H f ⁡ y = F ⁡ x H F ⁡ y
9 fveq1 ⊢ f = F → f ⁡ x G y = F ⁡ x G y
10 8 9 eqeq12d ⊢ f = F → f ⁡ x H f ⁡ y = f ⁡ x G y ↔ F ⁡ x H F ⁡ y = F ⁡ x G y
11 10 2ralbidv ⊢ f = F → ∀ 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
12 5 11 anbi12d ⊢ f = F → 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
13 12 1 elab2g ⊢ F ∈ V → F ∈ S ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
14 13 biimpd ⊢ F ∈ V → F ∈ S → F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
15 4 14 mpcom ⊢ F ∈ S → F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
16 rnexg ⊢ G ∈ GrpOp → ran ⁡ G ∈ V
17 fex ⊢ F : ran ⁡ G ⟶ ran ⁡ H ∧ ran ⁡ G ∈ V → F ∈ V
18 17 expcom ⊢ ran ⁡ G ∈ V → F : ran ⁡ G ⟶ ran ⁡ H → F ∈ V
19 16 18 syl ⊢ G ∈ GrpOp → F : ran ⁡ G ⟶ ran ⁡ H → F ∈ V
20 19 adantrd ⊢ G ∈ GrpOp → F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y → F ∈ V
21 13 biimprd ⊢ F ∈ V → F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y → F ∈ S
22 20 21 syli ⊢ G ∈ GrpOp → F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y → F ∈ S
23 15 22 impbid2 ⊢ G ∈ GrpOp → F ∈ S ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
24 23 adantr ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ S ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
25 3 24 bitrd ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ G GrpOpHom H ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y