Theorem ismhm 18753

Description: Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)

Hypotheses

Ref	Expression
ismhm.b	⊢ 𝐵 = (Base‘𝑆)
ismhm.c	⊢ 𝐶 = (Base‘𝑇)
ismhm.p	⊢ + = (+g‘𝑆)
ismhm.q	⊢ ⨣ = (+g‘𝑇)
ismhm.z	⊢ 0 = (0g‘𝑆)
ismhm.y	⊢ 𝑌 = (0g‘𝑇)

Assertion

Ref	Expression
ismhm	⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   + (𝑥,𝑦)   ⨣ (𝑥,𝑦)   𝑌(𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem ismhm

Dummy variables 𝑓 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mhm 18751	. . 3 ⊢ MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
2	1	elmpocl 7608	. 2 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd))
3		fveq2 6840	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
4		ismhm.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑇)
5	3, 4	eqtr4di 2789	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶)
6		fveq2 6840	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
7		ismhm.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
8	6, 7	eqtr4di 2789	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
9	5, 8	oveqan12rd 7387	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((Base‘𝑡) ↑m (Base‘𝑠)) = (𝐶 ↑m 𝐵))
10	8	adantr 480	. . . . . . . 8 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝐵)
11		fveq2 6840	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆))
12		ismhm.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑆)
13	11, 12	eqtr4di 2789	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + )
14	13	oveqd 7384	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (𝑥(+g‘𝑠)𝑦) = (𝑥 + 𝑦))
15	14	fveq2d 6844	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (𝑓‘(𝑥(+g‘𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦)))
16		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇))
17		ismhm.q	. . . . . . . . . . . 12 ⊢ ⨣ = (+g‘𝑇)
18	16, 17	eqtr4di 2789	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ )
19	18	oveqd 7384	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))
20	15, 19	eqeqan12d 2750	. . . . . . . . 9 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
21	10, 20	raleqbidv 3311	. . . . . . . 8 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
22	10, 21	raleqbidv 3311	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
23		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (0g‘𝑠) = (0g‘𝑆))
24		ismhm.z	. . . . . . . . . 10 ⊢ 0 = (0g‘𝑆)
25	23, 24	eqtr4di 2789	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (0g‘𝑠) = 0 )
26	25	fveq2d 6844	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (𝑓‘(0g‘𝑠)) = (𝑓‘ 0 ))
27		fveq2 6840	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → (0g‘𝑡) = (0g‘𝑇))
28		ismhm.y	. . . . . . . . 9 ⊢ 𝑌 = (0g‘𝑇)
29	27, 28	eqtr4di 2789	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (0g‘𝑡) = 𝑌)
30	26, 29	eqeqan12d 2750	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(0g‘𝑠)) = (0g‘𝑡) ↔ (𝑓‘ 0 ) = 𝑌))
31	22, 30	anbi12d 633	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡)) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)))
32	9, 31	rabeqbidv 3407	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))} = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)})
33		ovex 7400	. . . . . 6 ⊢ (𝐶 ↑m 𝐵) ∈ V
34	33	rabex 5280	. . . . 5 ⊢ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ∈ V
35	32, 1, 34	ovmpoa 7522	. . . 4 ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)})
36	35	eleq2d 2822	. . 3 ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)}))
37	4	fvexi 6854	. . . . . 6 ⊢ 𝐶 ∈ V
38	7	fvexi 6854	. . . . . 6 ⊢ 𝐵 ∈ V
39	37, 38	elmap 8819	. . . . 5 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶)
40	39	anbi1i 625	. . . 4 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)) ↔ (𝐹:𝐵⟶𝐶 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
41		fveq1 6839	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦)))
42		fveq1 6839	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
43		fveq1 6839	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦))
44	42, 43	oveq12d 7385	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))
45	41, 44	eqeq12d 2752	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
46	45	2ralbidv 3201	. . . . . 6 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
47		fveq1 6839	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘ 0 ) = (𝐹‘ 0 ))
48	47	eqeq1d 2738	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘ 0 ) = 𝑌 ↔ (𝐹‘ 0 ) = 𝑌))
49	46, 48	anbi12d 633	. . . . 5 ⊢ (𝑓 = 𝐹 → ((∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
50	49	elrab 3634	. . . 4 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
51		3anass 1095	. . . 4 ⊢ ((𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌) ↔ (𝐹:𝐵⟶𝐶 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
52	40, 50, 51	3bitr4i 303	. . 3 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ∧ (𝑓‘ 0 ) = 𝑌)} ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))
53	36, 52	bitrdi 287	. 2 ⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
54	2, 53	biadanii 822	1 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  {crab 3389  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ↑_m cmap 8773  Basecbs 17179  +_gcplusg 17220  0_gc0g 17402  Mndcmnd 18702   MndHom cmhm 18749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775  df-mhm 18751

This theorem is referenced by:  ismhmd  18754  mhmf  18757  ismhm0  18758  mhmismgmhm  18759  mhmpropd  18760  mhmlin  18761  mhm0  18762  idmhm  18763  mhmf1o  18764  0mhm  18787  resmhm  18788  resmhm2  18789  resmhm2b  18790  mhmco  18791  prdspjmhm  18797  pwsdiagmhm  18799  pwsco1mhm  18800  pwsco2mhm  18801  frmdup1  18832  mhmfmhm  19041  ghmmhm  19201  frgpmhm  19740  mulgmhm  19802  srglmhm  20202  srgrmhm  20203  c0mhm  20440  dfrhm2  20454  isrhm2d  20466  expmhm  21416  mat1mhm  22449  scmatmhm  22499  mat2pmatmhm  22698  pm2mpmhm  22785  dchrelbas3  27201  zringfrac  33614  xrge0iifmhm  34083  esumcocn  34224  elmrsubrn  35702  deg1mhm  43628