Theorem ismgmhm 18570

Description: Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.)

Hypotheses

Ref	Expression
ismgmhm.b	⊢ 𝐵 = (Base‘𝑆)
ismgmhm.c	⊢ 𝐶 = (Base‘𝑇)
ismgmhm.p	⊢ + = (+g‘𝑆)
ismgmhm.q	⊢ ⨣ = (+g‘𝑇)

Assertion

Ref	Expression
ismgmhm	⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))

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

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

Proof of Theorem ismgmhm

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

Step	Hyp	Ref	Expression
1		mgmhmrcl 18568	. 2 ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm))
2		fveq2 6822	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
3		ismgmhm.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑇)
4	2, 3	eqtr4di 2782	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶)
5		fveq2 6822	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
6		ismgmhm.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
7	5, 6	eqtr4di 2782	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
8	4, 7	oveqan12rd 7369	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((Base‘𝑡) ↑m (Base‘𝑠)) = (𝐶 ↑m 𝐵))
9	7	adantr 480	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝐵)
10		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆))
11		ismgmhm.p	. . . . . . . . . . . 12 ⊢ + = (+g‘𝑆)
12	10, 11	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + )
13	12	oveqd 7366	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (𝑥(+g‘𝑠)𝑦) = (𝑥 + 𝑦))
14	13	fveq2d 6826	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (𝑓‘(𝑥(+g‘𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦)))
15		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇))
16		ismgmhm.q	. . . . . . . . . . 11 ⊢ ⨣ = (+g‘𝑇)
17	15, 16	eqtr4di 2782	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ )
18	17	oveqd 7366	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))
19	14, 18	eqeqan12d 2743	. . . . . . . 8 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
20	9, 19	raleqbidv 3309	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
21	9, 20	raleqbidv 3309	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
22	8, 21	rabeqbidv 3413	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))} = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))})
23		df-mgmhm 18566	. . . . 5 ⊢ MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})
24		ovex 7382	. . . . . 6 ⊢ (𝐶 ↑m 𝐵) ∈ V
25	24	rabex 5278	. . . . 5 ⊢ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))} ∈ V
26	22, 23, 25	ovmpoa 7504	. . . 4 ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) → (𝑆 MgmHom 𝑇) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))})
27	26	eleq2d 2814	. . 3 ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))}))
28		fveq1 6821	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦)))
29		fveq1 6821	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
30		fveq1 6821	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦))
31	29, 30	oveq12d 7367	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))
32	28, 31	eqeq12d 2745	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
33	32	2ralbidv 3193	. . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
34	33	elrab 3648	. . . 4 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))} ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
35	3	fvexi 6836	. . . . . 6 ⊢ 𝐶 ∈ V
36	6	fvexi 6836	. . . . . 6 ⊢ 𝐵 ∈ V
37	35, 36	elmap 8798	. . . . 5 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶)
38	37	anbi1i 624	. . . 4 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
39	34, 38	bitri 275	. . 3 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))} ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
40	27, 39	bitrdi 287	. 2 ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))
41	1, 40	biadanii 821	1 ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  {crab 3394  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349   ↑_m cmap 8753  Basecbs 17120  +_gcplusg 17161  Mgmcmgm 18512   MgmHom cmgmhm 18564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-map 8755  df-mgmhm 18566

This theorem is referenced by:  mgmhmf  18571  mgmhmpropd  18572  mgmhmlin  18573  mgmhmf1o  18574  idmgmhm  18575  resmgmhm  18585  resmgmhm2  18586  resmgmhm2b  18587  mgmhmco  18588  ismhm0  18664  mhmismgmhm  18665  isrnghmmul  20327  c0mgm  20344  c0snmgmhm  20347