rhmimasubrnglem

Description: Lemma for rhmimasubrng : Modified part of mhmima . (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by AV, 16-Feb-2025)

		Ref	Expression
	Hypothesis	rhmimasubrnglem.b	$⊢ M = {mulGrp}_{R}$
	Assertion	rhmimasubrnglem	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]$

Proof

Step	Hyp	Ref	Expression
1		rhmimasubrnglem.b	$⊢ M = {mulGrp}_{R}$
2		simpll	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to F \in (M MndHom N)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3	subrngss	$⊢ X \in SubRng (R) \to X \subseteq {Base}_{R}$
5	1 3	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
6	4 5	sseqtrdi	$⊢ X \in SubRng (R) \to X \subseteq {Base}_{M}$
7	6	adantl	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to X \subseteq {Base}_{M}$
8	7	adantr	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to X \subseteq {Base}_{M}$
9		simprl	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to z \in X$
10	8 9	sseldd	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to z \in {Base}_{M}$
11		simprr	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to x \in X$
12	8 11	sseldd	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to x \in {Base}_{M}$
13		eqid	$⊢ {Base}_{M} = {Base}_{M}$
14		eqid	$⊢ +_{M} = +_{M}$
15		eqid	$⊢ +_{N} = +_{N}$
16	13 14 15	mhmlin	$⊢ (F \in (M MndHom N) \land z \in {Base}_{M} \land x \in {Base}_{M}) \to F (z +_{M} x) = F (z) +_{N} F (x)$
17	2 10 12 16	syl3anc	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to F (z +_{M} x) = F (z) +_{N} F (x)$
18		eqid	$⊢ {Base}_{N} = {Base}_{N}$
19	13 18	mhmf	$⊢ F \in (M MndHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
20	19	adantr	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to F : {Base}_{M} ⟶ {Base}_{N}$
21	20	ffnd	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to F Fn {Base}_{M}$
22	21	adantr	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to F Fn {Base}_{M}$
23		eqid	$⊢ \cdot_{R} = \cdot_{R}$
24	1 23	mgpplusg	$⊢ \cdot_{R} = +_{M}$
25	24	eqcomi	$⊢ +_{M} = \cdot_{R}$
26	25	subrngmcl	$⊢ (X \in SubRng (R) \land z \in X \land x \in X) \to z +_{M} x \in X$
27	26	3expb	$⊢ (X \in SubRng (R) \land (z \in X \land x \in X)) \to z +_{M} x \in X$
28	27	adantll	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to z +_{M} x \in X$
29		fnfvima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M} \land z +_{M} x \in X) \to F (z +_{M} x) \in F [X]$
30	22 8 28 29	syl3anc	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to F (z +_{M} x) \in F [X]$
31	17 30	eqeltrrd	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land (z \in X \land x \in X)) \to F (z) +_{N} F (x) \in F [X]$
32	31	anassrs	$⊢ (((F \in (M MndHom N) \land X \in SubRng (R)) \land z \in X) \land x \in X) \to F (z) +_{N} F (x) \in F [X]$
33	32	ralrimiva	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land z \in X) \to \forall x \in X F (z) +_{N} F (x) \in F [X]$
34		oveq2	$⊢ y = F (x) \to F (z) +_{N} y = F (z) +_{N} F (x)$
35	34	eleq1d	$⊢ y = F (x) \to (F (z) +_{N} y \in F [X] \leftrightarrow F (z) +_{N} F (x) \in F [X])$
36	35	ralima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M}) \to (\forall y \in F [X] F (z) +_{N} y \in F [X] \leftrightarrow \forall x \in X F (z) +_{N} F (x) \in F [X])$
37	21 7 36	syl2anc	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to (\forall y \in F [X] F (z) +_{N} y \in F [X] \leftrightarrow \forall x \in X F (z) +_{N} F (x) \in F [X])$
38	37	adantr	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land z \in X) \to (\forall y \in F [X] F (z) +_{N} y \in F [X] \leftrightarrow \forall x \in X F (z) +_{N} F (x) \in F [X])$
39	33 38	mpbird	$⊢ ((F \in (M MndHom N) \land X \in SubRng (R)) \land z \in X) \to \forall y \in F [X] F (z) +_{N} y \in F [X]$
40	39	ralrimiva	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X]$
41		oveq1	$⊢ x = F (z) \to x +_{N} y = F (z) +_{N} y$
42	41	eleq1d	$⊢ x = F (z) \to (x +_{N} y \in F [X] \leftrightarrow F (z) +_{N} y \in F [X])$
43	42	ralbidv	$⊢ x = F (z) \to (\forall y \in F [X] x +_{N} y \in F [X] \leftrightarrow \forall y \in F [X] F (z) +_{N} y \in F [X])$
44	43	ralima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M}) \to (\forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X] \leftrightarrow \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X])$
45	21 7 44	syl2anc	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to (\forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X] \leftrightarrow \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X])$
46	40 45	mpbird	$⊢ (F \in (M MndHom N) \land X \in SubRng (R)) \to \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]$

Metamath Proof Explorer

Theorem rhmimasubrnglem

Proof