Theorem ismgmhm 18786

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 18784	. 2 ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm))
2		fveq2 6885	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
3		ismgmhm.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑇)
4	2, 3	eqtr4di 2818	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶)
5		fveq2 6885	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
6		ismgmhm.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
7	5, 6	eqtr4di 2818	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
8	4, 7	oveqan12rd 7439	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((Base‘𝑡) ↑m (Base‘𝑠)) = (𝐶 ↑m 𝐵))
9	7	adantr 486	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (Base‘𝑠) = 𝐵)
10		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (+g‘𝑠) = (+g‘𝑆))
11		ismgmhm.p	. . . . . . . . . . . 12 ⊢ + = (+g‘𝑆)
12	10, 11	eqtr4di 2818	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (+g‘𝑠) = + )
13	12	oveqd 7436	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (𝑥(+g‘𝑠)𝑦) = (𝑥 + 𝑦))
14	13	fveq2d 6889	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (𝑓‘(𝑥(+g‘𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦)))
15		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (+g‘𝑡) = (+g‘𝑇))
16		ismgmhm.q	. . . . . . . . . . 11 ⊢ ⨣ = (+g‘𝑇)
17	15, 16	eqtr4di 2818	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (+g‘𝑡) = ⨣ )
18	17	oveqd 7436	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)))
19	14, 18	eqeqan12d 2779	. . . . . . . 8 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → ((𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
20	9, 19	raleqbidv 3340	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
21	9, 20	raleqbidv 3340	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))))
22	8, 21	rabeqbidv 3436	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))} = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))})
23		df-mgmhm 18782	. . . . 5 ⊢ MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})
24		ovex 7452	. . . . . 6 ⊢ (𝐶 ↑m 𝐵) ∈ V
25	24	rabex 5311	. . . . 5 ⊢ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))} ∈ V
26	22, 23, 25	ovmpoa 7574	. . . 4 ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) → (𝑆 MgmHom 𝑇) = {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))})
27	26	eleq2d 2851	. . 3 ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))}))
28		fveq1 6884	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦)))
29		fveq1 6884	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
30		fveq1 6884	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦))
31	29, 30	oveq12d 7437	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))
32	28, 31	eqeq12d 2781	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
33	32	2ralbidv 3231	. . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
34	33	elrab 3652	. . . 4 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))} ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
35	3	fvexi 6899	. . . . . 6 ⊢ 𝐶 ∈ V
36	6	fvexi 6899	. . . . . 6 ⊢ 𝐵 ∈ V
37	35, 36	elmap 8875	. . . . 5 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶)
38	37	anbi1i 636	. . . 4 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
39	34, 38	bitri 278	. . 3 ⊢ (𝐹 ∈ {𝑓 ∈ (𝐶 ↑m 𝐵) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓‘𝑥) ⨣ (𝑓‘𝑦))} ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))
40	27, 39	bitrdi 290	. 2 ⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))
41	1, 40	biadanii 834	1 ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  {crab 3418  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419   ↑_m cmap 8830  Basecbs 17291  +_gcplusg 17332  Mgmcmgm 18718   MgmHom cmgmhm 18780

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-map 8832  df-mgmhm 18782

This theorem is used by:  mgmhmf  18787  mgmhmpropd  18788  mgmhmlin  18789  mgmhmf1o  18790  idmgmhm  18791  resmgmhm  18801  resmgmhm2  18802  resmgmhm2b  18803  mgmhmco  18804  ismhm0  18885  mhmismgmhm  18886  isrnghmmul  20570  c0mgm  20587  c0snmgmhm  20590