isrnghm

Description: A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020)

	Ref	Expression
Hypotheses	isrnghm.b	$⊢ B = {Base}_{R}$
	isrnghm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	isrnghm.m	$⊢ \underset{˙}{*} = \cdot_{S}$
Assertion	isrnghm	$⊢ F \in (R RngHomo S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{*} F (y)))$

Proof

Step	Hyp	Ref	Expression
1		isrnghm.b	$⊢ B = {Base}_{R}$
2		isrnghm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		isrnghm.m	$⊢ \underset{˙}{*} = \cdot_{S}$
4		rnghmrcl	$⊢ F \in (R RngHomo S) \to (R \in Rng \land S \in Rng)$
5		eqid	$⊢ {Base}_{S} = {Base}_{S}$
6		eqid	$⊢ +_{R} = +_{R}$
7		eqid	$⊢ +_{S} = +_{S}$
8	1 2 3 5 6 7	rnghmval	$⊢ (R \in Rng \land S \in Rng) \to R RngHomo S = \{f \in ({Base}_{S}^{B}) \| \forall x \in B \forall y \in B (f (x +_{R} y) = f (x) +_{S} f (y) \land f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{*} f (y))\}$
9	8	eleq2d	$⊢ (R \in Rng \land S \in Rng) \to (F \in (R RngHomo S) \leftrightarrow F \in \{f \in ({Base}_{S}^{B}) \| \forall x \in B \forall y \in B (f (x +_{R} y) = f (x) +_{S} f (y) \land f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{*} f (y))\})$
10		fveq1	$⊢ f = F \to f (x +_{R} y) = F (x +_{R} y)$
11		fveq1	$⊢ f = F \to f (x) = F (x)$
12		fveq1	$⊢ f = F \to f (y) = F (y)$
13	11 12	oveq12d	$⊢ f = F \to f (x) +_{S} f (y) = F (x) +_{S} F (y)$
14	10 13	eqeq12d	$⊢ f = F \to (f (x +_{R} y) = f (x) +_{S} f (y) \leftrightarrow F (x +_{R} y) = F (x) +_{S} F (y))$
15		fveq1	$⊢ f = F \to f (x \underset{˙}{\cdot} y) = F (x \underset{˙}{\cdot} y)$
16	11 12	oveq12d	$⊢ f = F \to f (x) \underset{˙}{} f (y) = F (x) \underset{˙}{} F (y)$
17	15 16	eqeq12d	$⊢ f = F \to (f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{} f (y) \leftrightarrow F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y))$
18	14 17	anbi12d	$⊢ f = F \to ((f (x +_{R} y) = f (x) +_{S} f (y) \land f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{} f (y)) \leftrightarrow (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
19	18	2ralbidv	$⊢ f = F \to (\forall x \in B \forall y \in B (f (x +_{R} y) = f (x) +_{S} f (y) \land f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{} f (y)) \leftrightarrow \forall x \in B \forall y \in B (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
20	19	elrab	$⊢ F \in \{f \in ({Base}_{S}^{B}) \| \forall x \in B \forall y \in B (f (x +_{R} y) = f (x) +_{S} f (y) \land f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{} f (y))\} \leftrightarrow (F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
21		r19.26-2	$⊢ \forall x \in B \forall y \in B (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)) \leftrightarrow (\forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y))$
22	21	anbi2i	$⊢ (F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y))) \leftrightarrow (F \in ({Base}_{S}^{B}) \land (\forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
23		anass	$⊢ ((F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)) \leftrightarrow (F \in ({Base}_{S}^{B}) \land (\forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
24	22 23	bitr4i	$⊢ (F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y))) \leftrightarrow ((F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y))$
25	1 5 6 7	isghm	$⊢ F \in (R GrpHom S) \leftrightarrow ((R \in Grp \land S \in Grp) \land (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)))$
26		fvex	$⊢ {Base}_{S} \in V$
27	1	fvexi	$⊢ B \in V$
28	26 27	pm3.2i	$⊢ ({Base}_{S} \in V \land B \in V)$
29		elmapg	$⊢ ({Base}_{S} \in V \land B \in V) \to (F \in ({Base}_{S}^{B}) \leftrightarrow F : B ⟶ {Base}_{S})$
30	28 29	mp1i	$⊢ (R \in Rng \land S \in Rng) \to (F \in ({Base}_{S}^{B}) \leftrightarrow F : B ⟶ {Base}_{S})$
31	30	anbi1d	$⊢ (R \in Rng \land S \in Rng) \to ((F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \leftrightarrow (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)))$
32		rngabl	$⊢ R \in Rng \to R \in Abel$
33		ablgrp	$⊢ R \in Abel \to R \in Grp$
34	32 33	syl	$⊢ R \in Rng \to R \in Grp$
35		rngabl	$⊢ S \in Rng \to S \in Abel$
36		ablgrp	$⊢ S \in Abel \to S \in Grp$
37	35 36	syl	$⊢ S \in Rng \to S \in Grp$
38		ibar	$⊢ (R \in Grp \land S \in Grp) \to ((F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \leftrightarrow ((R \in Grp \land S \in Grp) \land (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y))))$
39	34 37 38	syl2an	$⊢ (R \in Rng \land S \in Rng) \to ((F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \leftrightarrow ((R \in Grp \land S \in Grp) \land (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y))))$
40	31 39	bitr2d	$⊢ (R \in Rng \land S \in Rng) \to (((R \in Grp \land S \in Grp) \land (F : B ⟶ {Base}_{S} \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y))) \leftrightarrow (F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)))$
41	25 40	bitr2id	$⊢ (R \in Rng \land S \in Rng) \to ((F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \leftrightarrow F \in (R GrpHom S))$
42	41	anbi1d	$⊢ (R \in Rng \land S \in Rng) \to (((F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B F (x +_{R} y) = F (x) +_{S} F (y)) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)) \leftrightarrow (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
43	24 42	bitrid	$⊢ (R \in Rng \land S \in Rng) \to ((F \in ({Base}_{S}^{B}) \land \forall x \in B \forall y \in B (F (x +_{R} y) = F (x) +_{S} F (y) \land F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y))) \leftrightarrow (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
44	20 43	bitrid	$⊢ (R \in Rng \land S \in Rng) \to (F \in \{f \in ({Base}_{S}^{B}) \| \forall x \in B \forall y \in B (f (x +_{R} y) = f (x) +_{S} f (y) \land f (x \underset{˙}{\cdot} y) = f (x) \underset{˙}{} f (y))\} \leftrightarrow (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{} F (y)))$
45	9 44	bitrd	$⊢ (R \in Rng \land S \in Rng) \to (F \in (R RngHomo S) \leftrightarrow (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{*} F (y)))$
46	4 45	biadanii	$⊢ F \in (R RngHomo S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{*} F (y)))$

Metamath Proof Explorer

Theorem isrnghm

Proof