Theorem mhmeql 13598

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.

Step	Hyp	Ref	Expression
1		eqid 2230	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
2		eqid 2230	. . . . . 6 ⊢ (Base‘𝑇) = (Base‘𝑇)
3	1, 2	mhmf 13571	. . . . 5 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
4	3	adantr 276	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
5	4	ffnd 5485	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐹 Fn (Base‘𝑆))
6	1, 2	mhmf 13571	. . . . 5 ⊢ (𝐺 ∈ (𝑆 MndHom 𝑇) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇))
7	6	adantl 277	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇))
8	7	ffnd 5485	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐺 Fn (Base‘𝑆))
9		fndmin 5757	. . 3 ⊢ ((𝐹 Fn (Base‘𝑆) ∧ 𝐺 Fn (Base‘𝑆)) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
10	5, 8, 9	syl2anc 411	. 2 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
11		ssrab2 3311	. . . 4 ⊢ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ⊆ (Base‘𝑆)
12	11	a1i 9	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ⊆ (Base‘𝑆))
13		fveq2 5642	. . . . 5 ⊢ (𝑧 = (0g‘𝑆) → (𝐹‘𝑧) = (𝐹‘(0g‘𝑆)))
14		fveq2 5642	. . . . 5 ⊢ (𝑧 = (0g‘𝑆) → (𝐺‘𝑧) = (𝐺‘(0g‘𝑆)))
15	13, 14	eqeq12d 2245	. . . 4 ⊢ (𝑧 = (0g‘𝑆) → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘(0g‘𝑆)) = (𝐺‘(0g‘𝑆))))
16		mhmrcl1 13569	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd)
17	16	adantr 276	. . . . 5 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝑆 ∈ Mnd)
18		eqid 2230	. . . . . 6 ⊢ (0g‘𝑆) = (0g‘𝑆)
19	1, 18	mndidcl 13536	. . . . 5 ⊢ (𝑆 ∈ Mnd → (0g‘𝑆) ∈ (Base‘𝑆))
20	17, 19	syl 14	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (0g‘𝑆) ∈ (Base‘𝑆))
21		eqid 2230	. . . . . . 7 ⊢ (0g‘𝑇) = (0g‘𝑇)
22	18, 21	mhm0 13574	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇))
23	22	adantr 276	. . . . 5 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇))
24	18, 21	mhm0 13574	. . . . . 6 ⊢ (𝐺 ∈ (𝑆 MndHom 𝑇) → (𝐺‘(0g‘𝑆)) = (0g‘𝑇))
25	24	adantl 277	. . . . 5 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐺‘(0g‘𝑆)) = (0g‘𝑇))
26	23, 25	eqtr4d 2266	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g‘𝑆)) = (𝐺‘(0g‘𝑆)))
27	15, 20, 26	elrabd 2963	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (0g‘𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
28		fveq2 5642	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑥(+g‘𝑆)𝑦) → (𝐹‘𝑧) = (𝐹‘(𝑥(+g‘𝑆)𝑦)))
29		fveq2 5642	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑥(+g‘𝑆)𝑦) → (𝐺‘𝑧) = (𝐺‘(𝑥(+g‘𝑆)𝑦)))
30	28, 29	eqeq12d 2245	. . . . . . . . . 10 ⊢ (𝑧 = (𝑥(+g‘𝑆)𝑦) → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘(𝑥(+g‘𝑆)𝑦)) = (𝐺‘(𝑥(+g‘𝑆)𝑦))))
31	17	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑆 ∈ Mnd)
32		simplrl 537	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑥 ∈ (Base‘𝑆))
33		simprl 531	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑦 ∈ (Base‘𝑆))
34		eqid 2230	. . . . . . . . . . . 12 ⊢ (+g‘𝑆) = (+g‘𝑆)
35	1, 34	mndcl 13529	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆))
36	31, 32, 33, 35	syl3anc 1273	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆))
37		simplll 535	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝐹 ∈ (𝑆 MndHom 𝑇))
38		eqid 2230	. . . . . . . . . . . . 13 ⊢ (+g‘𝑇) = (+g‘𝑇)
39	1, 34, 38	mhmlin 13573	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)))
40	37, 32, 33, 39	syl3anc 1273	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)))
41		simpllr 536	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝐺 ∈ (𝑆 MndHom 𝑇))
42	1, 34, 38	mhmlin 13573	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐺‘(𝑥(+g‘𝑆)𝑦)) = ((𝐺‘𝑥)(+g‘𝑇)(𝐺‘𝑦)))
43	41, 32, 33, 42	syl3anc 1273	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐺‘(𝑥(+g‘𝑆)𝑦)) = ((𝐺‘𝑥)(+g‘𝑇)(𝐺‘𝑦)))
44		simplrr 538	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘𝑥) = (𝐺‘𝑥))
45		simprr 533	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘𝑦) = (𝐺‘𝑦))
46	44, 45	oveq12d 6041	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) = ((𝐺‘𝑥)(+g‘𝑇)(𝐺‘𝑦)))
47	43, 46	eqtr4d 2266	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐺‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)))
48	40, 47	eqtr4d 2266	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = (𝐺‘(𝑥(+g‘𝑆)𝑦)))
49	30, 36, 48	elrabd 2963	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
50	49	expr 375	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
51	50	ralrimiva 2604	. . . . . . 7 ⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
52		fveq2 5642	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦))
53		fveq2 5642	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝐺‘𝑧) = (𝐺‘𝑦))
54	52, 53	eqeq12d 2245	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘𝑦) = (𝐺‘𝑦)))
55	54	ralrab 2966	. . . . . . 7 ⊢ (∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ↔ ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
56	51, 55	sylibr 134	. . . . . 6 ⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
57	56	expr 375	. . . . 5 ⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ 𝑥 ∈ (Base‘𝑆)) → ((𝐹‘𝑥) = (𝐺‘𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
58	57	ralrimiva 2604	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)((𝐹‘𝑥) = (𝐺‘𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
59		fveq2 5642	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥))
60		fveq2 5642	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥))
61	59, 60	eqeq12d 2245	. . . . 5 ⊢ (𝑧 = 𝑥 → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
62	61	ralrab 2966	. . . 4 ⊢ (∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ↔ ∀𝑥 ∈ (Base‘𝑆)((𝐹‘𝑥) = (𝐺‘𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
63	58, 62	sylibr 134	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
64	1, 18, 34	issubm 13578	. . . 4 ⊢ (𝑆 ∈ Mnd → ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ∈ (SubMnd‘𝑆) ↔ ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ⊆ (Base‘𝑆) ∧ (0g‘𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ∧ ∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})))
65	17, 64	syl 14	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ∈ (SubMnd‘𝑆) ↔ ({𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ⊆ (Base‘𝑆) ∧ (0g‘𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ∧ ∀𝑥 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})))
66	12, 27, 63, 65	mpbir3and 1206	. 2 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ∈ (SubMnd‘𝑆))
67	10, 66	eqeltrd 2307	1 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1004   = wceq 1397   ∈ wcel 2201  ∀wral 2509  {crab 2513   ∩ cin 3198   ⊆ wss 3199  dom cdm 4727   Fn wfn 5323  ⟶wf 5324  ‘cfv 5328  (class class class)co 6023  Basecbs 13105  +_gcplusg 13183  0_gc0g 13362  Mndcmnd 13522   MndHom cmhm 13563  SubMndcsubmnd 13564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-cnex 8128  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-ral 2514  df-rex 2515  df-reu 2516  df-rmo 2517  df-rab 2518  df-v 2803  df-sbc 3031  df-csb 3127  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-iun 3973  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-fv 5336  df-riota 5976  df-ov 6026  df-oprab 6027  df-mpo 6028  df-1st 6308  df-2nd 6309  df-map 6824  df-inn 9149  df-2 9207  df-ndx 13108  df-slot 13109  df-base 13111  df-plusg 13196  df-0g 13364  df-mgm 13462  df-sgrp 13508  df-mnd 13523  df-mhm 13565  df-submnd 13566

This theorem is referenced by:  ghmeql  13877  rhmeql  14288