MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mhmeql Structured version   Visualization version   GIF version

Theorem mhmeql 17679
Description: The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
Assertion
Ref Expression
mhmeql ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹𝐺) ∈ (SubMnd‘𝑆))

Proof of Theorem mhmeql
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2799 . . . . . 6 (Base‘𝑆) = (Base‘𝑆)
2 eqid 2799 . . . . . 6 (Base‘𝑇) = (Base‘𝑇)
31, 2mhmf 17655 . . . . 5 (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
43adantr 473 . . . 4 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
54ffnd 6257 . . 3 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐹 Fn (Base‘𝑆))
61, 2mhmf 17655 . . . . 5 (𝐺 ∈ (𝑆 MndHom 𝑇) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇))
76adantl 474 . . . 4 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇))
87ffnd 6257 . . 3 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐺 Fn (Base‘𝑆))
9 fndmin 6550 . . 3 ((𝐹 Fn (Base‘𝑆) ∧ 𝐺 Fn (Base‘𝑆)) → dom (𝐹𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})
105, 8, 9syl2anc 580 . 2 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})
11 ssrab2 3883 . . . 4 {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ⊆ (Base‘𝑆)
1211a1i 11 . . 3 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ⊆ (Base‘𝑆))
13 mhmrcl1 17653 . . . . . 6 (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd)
1413adantr 473 . . . . 5 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝑆 ∈ Mnd)
15 eqid 2799 . . . . . 6 (0g𝑆) = (0g𝑆)
161, 15mndidcl 17623 . . . . 5 (𝑆 ∈ Mnd → (0g𝑆) ∈ (Base‘𝑆))
1714, 16syl 17 . . . 4 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (0g𝑆) ∈ (Base‘𝑆))
18 eqid 2799 . . . . . . 7 (0g𝑇) = (0g𝑇)
1915, 18mhm0 17658 . . . . . 6 (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘(0g𝑆)) = (0g𝑇))
2019adantr 473 . . . . 5 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g𝑆)) = (0g𝑇))
2115, 18mhm0 17658 . . . . . 6 (𝐺 ∈ (𝑆 MndHom 𝑇) → (𝐺‘(0g𝑆)) = (0g𝑇))
2221adantl 474 . . . . 5 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐺‘(0g𝑆)) = (0g𝑇))
2320, 22eqtr4d 2836 . . . 4 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g𝑆)) = (𝐺‘(0g𝑆)))
24 fveq2 6411 . . . . . 6 (𝑧 = (0g𝑆) → (𝐹𝑧) = (𝐹‘(0g𝑆)))
25 fveq2 6411 . . . . . 6 (𝑧 = (0g𝑆) → (𝐺𝑧) = (𝐺‘(0g𝑆)))
2624, 25eqeq12d 2814 . . . . 5 (𝑧 = (0g𝑆) → ((𝐹𝑧) = (𝐺𝑧) ↔ (𝐹‘(0g𝑆)) = (𝐺‘(0g𝑆))))
2726elrab 3556 . . . 4 ((0g𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ↔ ((0g𝑆) ∈ (Base‘𝑆) ∧ (𝐹‘(0g𝑆)) = (𝐺‘(0g𝑆))))
2817, 23, 27sylanbrc 579 . . 3 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (0g𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})
2914ad2antrr 718 . . . . . . . . . . 11 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → 𝑆 ∈ Mnd)
30 simplrl 796 . . . . . . . . . . 11 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → 𝑥 ∈ (Base‘𝑆))
31 simprl 788 . . . . . . . . . . 11 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → 𝑦 ∈ (Base‘𝑆))
32 eqid 2799 . . . . . . . . . . . 12 (+g𝑆) = (+g𝑆)
331, 32mndcl 17616 . . . . . . . . . . 11 ((𝑆 ∈ Mnd ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+g𝑆)𝑦) ∈ (Base‘𝑆))
3429, 30, 31, 33syl3anc 1491 . . . . . . . . . 10 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝑥(+g𝑆)𝑦) ∈ (Base‘𝑆))
35 simplll 792 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → 𝐹 ∈ (𝑆 MndHom 𝑇))
36 eqid 2799 . . . . . . . . . . . . 13 (+g𝑇) = (+g𝑇)
371, 32, 36mhmlin 17657 . . . . . . . . . . . 12 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g𝑆)𝑦)) = ((𝐹𝑥)(+g𝑇)(𝐹𝑦)))
3835, 30, 31, 37syl3anc 1491 . . . . . . . . . . 11 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝐹‘(𝑥(+g𝑆)𝑦)) = ((𝐹𝑥)(+g𝑇)(𝐹𝑦)))
39 simpllr 794 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → 𝐺 ∈ (𝑆 MndHom 𝑇))
401, 32, 36mhmlin 17657 . . . . . . . . . . . . 13 ((𝐺 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐺‘(𝑥(+g𝑆)𝑦)) = ((𝐺𝑥)(+g𝑇)(𝐺𝑦)))
4139, 30, 31, 40syl3anc 1491 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝐺‘(𝑥(+g𝑆)𝑦)) = ((𝐺𝑥)(+g𝑇)(𝐺𝑦)))
42 simplrr 797 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝐹𝑥) = (𝐺𝑥))
43 simprr 790 . . . . . . . . . . . . 13 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝐹𝑦) = (𝐺𝑦))
4442, 43oveq12d 6896 . . . . . . . . . . . 12 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → ((𝐹𝑥)(+g𝑇)(𝐹𝑦)) = ((𝐺𝑥)(+g𝑇)(𝐺𝑦)))
4541, 44eqtr4d 2836 . . . . . . . . . . 11 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝐺‘(𝑥(+g𝑆)𝑦)) = ((𝐹𝑥)(+g𝑇)(𝐹𝑦)))
4638, 45eqtr4d 2836 . . . . . . . . . 10 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝐹‘(𝑥(+g𝑆)𝑦)) = (𝐺‘(𝑥(+g𝑆)𝑦)))
47 fveq2 6411 . . . . . . . . . . . 12 (𝑧 = (𝑥(+g𝑆)𝑦) → (𝐹𝑧) = (𝐹‘(𝑥(+g𝑆)𝑦)))
48 fveq2 6411 . . . . . . . . . . . 12 (𝑧 = (𝑥(+g𝑆)𝑦) → (𝐺𝑧) = (𝐺‘(𝑥(+g𝑆)𝑦)))
4947, 48eqeq12d 2814 . . . . . . . . . . 11 (𝑧 = (𝑥(+g𝑆)𝑦) → ((𝐹𝑧) = (𝐺𝑧) ↔ (𝐹‘(𝑥(+g𝑆)𝑦)) = (𝐺‘(𝑥(+g𝑆)𝑦))))
5049elrab 3556 . . . . . . . . . 10 ((𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ↔ ((𝑥(+g𝑆)𝑦) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑥(+g𝑆)𝑦)) = (𝐺‘(𝑥(+g𝑆)𝑦))))
5134, 46, 50sylanbrc 579 . . . . . . . . 9 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹𝑦) = (𝐺𝑦))) → (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})
5251expr 449 . . . . . . . 8 ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹𝑦) = (𝐺𝑦) → (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}))
5352ralrimiva 3147 . . . . . . 7 (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) → ∀𝑦 ∈ (Base‘𝑆)((𝐹𝑦) = (𝐺𝑦) → (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}))
54 fveq2 6411 . . . . . . . . 9 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
55 fveq2 6411 . . . . . . . . 9 (𝑧 = 𝑦 → (𝐺𝑧) = (𝐺𝑦))
5654, 55eqeq12d 2814 . . . . . . . 8 (𝑧 = 𝑦 → ((𝐹𝑧) = (𝐺𝑧) ↔ (𝐹𝑦) = (𝐺𝑦)))
5756ralrab 3562 . . . . . . 7 (∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ↔ ∀𝑦 ∈ (Base‘𝑆)((𝐹𝑦) = (𝐺𝑦) → (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}))
5853, 57sylibr 226 . . . . . 6 (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹𝑥) = (𝐺𝑥))) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})
5958expr 449 . . . . 5 (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ 𝑥 ∈ (Base‘𝑆)) → ((𝐹𝑥) = (𝐺𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}))
6059ralrimiva 3147 . . . 4 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)((𝐹𝑥) = (𝐺𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}))
61 fveq2 6411 . . . . . 6 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
62 fveq2 6411 . . . . . 6 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
6361, 62eqeq12d 2814 . . . . 5 (𝑧 = 𝑥 → ((𝐹𝑧) = (𝐺𝑧) ↔ (𝐹𝑥) = (𝐺𝑥)))
6463ralrab 3562 . . . 4 (∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ↔ ∀𝑥 ∈ (Base‘𝑆)((𝐹𝑥) = (𝐺𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}))
6560, 64sylibr 226 . . 3 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})
661, 15, 32issubm 17662 . . . 4 (𝑆 ∈ Mnd → ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ∈ (SubMnd‘𝑆) ↔ ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ⊆ (Base‘𝑆) ∧ (0g𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ∧ ∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})))
6714, 66syl 17 . . 3 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ∈ (SubMnd‘𝑆) ↔ ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ⊆ (Base‘𝑆) ∧ (0g𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ∧ ∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} (𝑥(+g𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)})))
6812, 28, 65, 67mpbir3and 1443 . 2 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → {𝑧 ∈ (Base‘𝑆) ∣ (𝐹𝑧) = (𝐺𝑧)} ∈ (SubMnd‘𝑆))
6910, 68eqeltrd 2878 1 ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹𝐺) ∈ (SubMnd‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157  wral 3089  {crab 3093  cin 3768  wss 3769  dom cdm 5312   Fn wfn 6096  wf 6097  cfv 6101  (class class class)co 6878  Basecbs 16184  +gcplusg 16267  0gc0g 16415  Mndcmnd 17609   MndHom cmhm 17648  SubMndcsubmnd 17649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-riota 6839  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-map 8097  df-0g 16417  df-mgm 17557  df-sgrp 17599  df-mnd 17610  df-mhm 17650  df-submnd 17651
This theorem is referenced by:  ghmeql  17996  rhmeql  19128
  Copyright terms: Public domain W3C validator