Theorem mhmeql 13491

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 2209	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
2		eqid 2209	. . . . . 6 ⊢ (Base‘𝑇) = (Base‘𝑇)
3	1, 2	mhmf 13464	. . . . 5 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
4	3	adantr 276	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇))
5	4	ffnd 5450	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐹 Fn (Base‘𝑆))
6	1, 2	mhmf 13464	. . . . 5 ⊢ (𝐺 ∈ (𝑆 MndHom 𝑇) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇))
7	6	adantl 277	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇))
8	7	ffnd 5450	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝐺 Fn (Base‘𝑆))
9		fndmin 5715	. . 3 ⊢ ((𝐹 Fn (Base‘𝑆) ∧ 𝐺 Fn (Base‘𝑆)) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
10	5, 8, 9	syl2anc 411	. 2 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
11		ssrab2 3289	. . . 4 ⊢ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ⊆ (Base‘𝑆)
12	11	a1i 9	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ⊆ (Base‘𝑆))
13		fveq2 5603	. . . . 5 ⊢ (𝑧 = (0g‘𝑆) → (𝐹‘𝑧) = (𝐹‘(0g‘𝑆)))
14		fveq2 5603	. . . . 5 ⊢ (𝑧 = (0g‘𝑆) → (𝐺‘𝑧) = (𝐺‘(0g‘𝑆)))
15	13, 14	eqeq12d 2224	. . . 4 ⊢ (𝑧 = (0g‘𝑆) → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘(0g‘𝑆)) = (𝐺‘(0g‘𝑆))))
16		mhmrcl1 13462	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd)
17	16	adantr 276	. . . . 5 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → 𝑆 ∈ Mnd)
18		eqid 2209	. . . . . 6 ⊢ (0g‘𝑆) = (0g‘𝑆)
19	1, 18	mndidcl 13429	. . . . 5 ⊢ (𝑆 ∈ Mnd → (0g‘𝑆) ∈ (Base‘𝑆))
20	17, 19	syl 14	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (0g‘𝑆) ∈ (Base‘𝑆))
21		eqid 2209	. . . . . . 7 ⊢ (0g‘𝑇) = (0g‘𝑇)
22	18, 21	mhm0 13467	. . . . . 6 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇))
23	22	adantr 276	. . . . 5 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇))
24	18, 21	mhm0 13467	. . . . . 6 ⊢ (𝐺 ∈ (𝑆 MndHom 𝑇) → (𝐺‘(0g‘𝑆)) = (0g‘𝑇))
25	24	adantl 277	. . . . 5 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐺‘(0g‘𝑆)) = (0g‘𝑇))
26	23, 25	eqtr4d 2245	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g‘𝑆)) = (𝐺‘(0g‘𝑆)))
27	15, 20, 26	elrabd 2941	. . 3 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (0g‘𝑆) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
28		fveq2 5603	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑥(+g‘𝑆)𝑦) → (𝐹‘𝑧) = (𝐹‘(𝑥(+g‘𝑆)𝑦)))
29		fveq2 5603	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑥(+g‘𝑆)𝑦) → (𝐺‘𝑧) = (𝐺‘(𝑥(+g‘𝑆)𝑦)))
30	28, 29	eqeq12d 2224	. . . . . . . . . 10 ⊢ (𝑧 = (𝑥(+g‘𝑆)𝑦) → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘(𝑥(+g‘𝑆)𝑦)) = (𝐺‘(𝑥(+g‘𝑆)𝑦))))
31	17	ad2antrr 488	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑆 ∈ Mnd)
32		simplrl 535	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑥 ∈ (Base‘𝑆))
33		simprl 529	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑦 ∈ (Base‘𝑆))
34		eqid 2209	. . . . . . . . . . . 12 ⊢ (+g‘𝑆) = (+g‘𝑆)
35	1, 34	mndcl 13422	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Mnd ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆))
36	31, 32, 33, 35	syl3anc 1252	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆))
37		simplll 533	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝐹 ∈ (𝑆 MndHom 𝑇))
38		eqid 2209	. . . . . . . . . . . . 13 ⊢ (+g‘𝑇) = (+g‘𝑇)
39	1, 34, 38	mhmlin 13466	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)))
40	37, 32, 33, 39	syl3anc 1252	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)))
41		simpllr 534	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝐺 ∈ (𝑆 MndHom 𝑇))
42	1, 34, 38	mhmlin 13466	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐺‘(𝑥(+g‘𝑆)𝑦)) = ((𝐺‘𝑥)(+g‘𝑇)(𝐺‘𝑦)))
43	41, 32, 33, 42	syl3anc 1252	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐺‘(𝑥(+g‘𝑆)𝑦)) = ((𝐺‘𝑥)(+g‘𝑇)(𝐺‘𝑦)))
44		simplrr 536	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘𝑥) = (𝐺‘𝑥))
45		simprr 531	. . . . . . . . . . . . 13 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘𝑦) = (𝐺‘𝑦))
46	44, 45	oveq12d 5992	. . . . . . . . . . . 12 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) = ((𝐺‘𝑥)(+g‘𝑇)(𝐺‘𝑦)))
47	43, 46	eqtr4d 2245	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐺‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)))
48	40, 47	eqtr4d 2245	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = (𝐺‘(𝑥(+g‘𝑆)𝑦)))
49	30, 36, 48	elrabd 2941	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})
50	49	expr 375	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
51	50	ralrimiva 2583	. . . . . . 7 ⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
52		fveq2 5603	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦))
53		fveq2 5603	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝐺‘𝑧) = (𝐺‘𝑦))
54	52, 53	eqeq12d 2224	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘𝑦) = (𝐺‘𝑦)))
55	54	ralrab 2944	. . . . . . 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 2583	. . . 4 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)((𝐹‘𝑥) = (𝐺‘𝑥) → ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥(+g‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))
59		fveq2 5603	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥))
60		fveq2 5603	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥))
61	59, 60	eqeq12d 2224	. . . . 5 ⊢ (𝑧 = 𝑥 → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
62	61	ralrab 2944	. . . 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 13471	. . . 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 1185	. 2 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ∈ (SubMnd‘𝑆))
67	10, 66	eqeltrd 2286	1 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 983   = wceq 1375   ∈ wcel 2180  ∀wral 2488  {crab 2492   ∩ cin 3176   ⊆ wss 3177  dom cdm 4696   Fn wfn 5289  ⟶wf 5290  ‘cfv 5294  (class class class)co 5974  Basecbs 12998  +_gcplusg 13076  0_gc0g 13255  Mndcmnd 13415   MndHom cmhm 13456  SubMndcsubmnd 13457

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 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-cnex 8058  ax-resscn 8059  ax-1re 8061  ax-addrcl 8064

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-rex 2494  df-reu 2495  df-rmo 2496  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-map 6767  df-inn 9079  df-2 9137  df-ndx 13001  df-slot 13002  df-base 13004  df-plusg 13089  df-0g 13257  df-mgm 13355  df-sgrp 13401  df-mnd 13416  df-mhm 13458  df-submnd 13459

This theorem is referenced by:  ghmeql  13770  rhmeql  14179