Proof of Theorem elghomlem2OLD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elghomlem1OLD.1 | . . . 4
⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} | 
| 2 | 1 | elghomlem1OLD 37892 | . . 3
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆) | 
| 3 | 2 | eleq2d 2827 | . 2
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ 𝐹 ∈ 𝑆)) | 
| 4 |  | elex 3501 | . . . . 5
⊢ (𝐹 ∈ 𝑆 → 𝐹 ∈ V) | 
| 5 |  | feq1 6716 | . . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓:ran 𝐺⟶ran 𝐻 ↔ 𝐹:ran 𝐺⟶ran 𝐻)) | 
| 6 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) | 
| 7 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦)) | 
| 8 | 6, 7 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = ((𝐹‘𝑥)𝐻(𝐹‘𝑦))) | 
| 9 |  | fveq1 6905 | . . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥𝐺𝑦)) = (𝐹‘(𝑥𝐺𝑦))) | 
| 10 | 8, 9 | eqeq12d 2753 | . . . . . . . . 9
⊢ (𝑓 = 𝐹 → (((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)) ↔ ((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))) | 
| 11 | 10 | 2ralbidv 3221 | . . . . . . . 8
⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)) ↔ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))) | 
| 12 | 5, 11 | anbi12d 632 | . . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦))) ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | 
| 13 | 12, 1 | elab2g 3680 | . . . . . 6
⊢ (𝐹 ∈ V → (𝐹 ∈ 𝑆 ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | 
| 14 | 13 | biimpd 229 | . . . . 5
⊢ (𝐹 ∈ V → (𝐹 ∈ 𝑆 → (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | 
| 15 | 4, 14 | mpcom 38 | . . . 4
⊢ (𝐹 ∈ 𝑆 → (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))) | 
| 16 |  | rnexg 7924 | . . . . . . 7
⊢ (𝐺 ∈ GrpOp → ran 𝐺 ∈ V) | 
| 17 |  | fex 7246 | . . . . . . . 8
⊢ ((𝐹:ran 𝐺⟶ran 𝐻 ∧ ran 𝐺 ∈ V) → 𝐹 ∈ V) | 
| 18 | 17 | expcom 413 | . . . . . . 7
⊢ (ran
𝐺 ∈ V → (𝐹:ran 𝐺⟶ran 𝐻 → 𝐹 ∈ V)) | 
| 19 | 16, 18 | syl 17 | . . . . . 6
⊢ (𝐺 ∈ GrpOp → (𝐹:ran 𝐺⟶ran 𝐻 → 𝐹 ∈ V)) | 
| 20 | 19 | adantrd 491 | . . . . 5
⊢ (𝐺 ∈ GrpOp → ((𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))) → 𝐹 ∈ V)) | 
| 21 | 13 | biimprd 248 | . . . . 5
⊢ (𝐹 ∈ V → ((𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))) → 𝐹 ∈ 𝑆)) | 
| 22 | 20, 21 | syli 39 | . . . 4
⊢ (𝐺 ∈ GrpOp → ((𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))) → 𝐹 ∈ 𝑆)) | 
| 23 | 15, 22 | impbid2 226 | . . 3
⊢ (𝐺 ∈ GrpOp → (𝐹 ∈ 𝑆 ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | 
| 24 | 23 | adantr 480 | . 2
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ 𝑆 ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) | 
| 25 | 3, 24 | bitrd 279 | 1
⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦))))) |