Theorem 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={\mathrm{mulGrp}}_R$$
Assertion	rhmimasubrnglem	Could not format assertion : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rhmimasubrnglem.b	$$⊢M={\mathrm{mulGrp}}_R$$
2		simpll	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> F e. ( M MndHom N ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> F e. ( M MndHom N ) ) with typecode |-
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3	subrngss	Could not format ( X e. ( SubRng ` R ) -> X C_ ( Base ` R ) ) : No typesetting found for |- ( X e. ( SubRng ` R ) -> X C_ ( Base ` R ) ) with typecode |-
5	1 3	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_M$$
6	4 5	sseqtrdi	Could not format ( X e. ( SubRng ` R ) -> X C_ ( Base ` M ) ) : No typesetting found for |- ( X e. ( SubRng ` R ) -> X C_ ( Base ` M ) ) with typecode |-
7	6	adantl	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> X C_ ( Base ` M ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> X C_ ( Base ` M ) ) with typecode |-
8	7	adantr	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> X C_ ( Base ` M ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> X C_ ( Base ` M ) ) with typecode |-
9		simprl	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> z e. X ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> z e. X ) with typecode |-
10	8 9	sseldd	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> z e. ( Base ` M ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> z e. ( Base ` M ) ) with typecode |-
11		simprr	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> x e. X ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> x e. X ) with typecode |-
12	8 11	sseldd	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> x e. ( Base ` M ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> x e. ( Base ` M ) ) with typecode |-
13		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
14		eqid	$$⊢{+}_M={+}_M$$
15		eqid	$$⊢{+}_N={+}_N$$
16	13 14 15	mhmlin	$$⊢\left(F\in \left(M\mathrm{MndHom}N\right)\wedge z\in {\mathrm{Base}}_M\wedge x\in {\mathrm{Base}}_M\right)\to F\left(z{+}_{M}x\right)=F\left(z\right){+}_{N}F\left(x\right)$$
17	2 10 12 16	syl3anc	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) ) with typecode |-
18		eqid	$$⊢{\mathrm{Base}}_N={\mathrm{Base}}_N$$
19	13 18	mhmf	$$⊢F\in \left(M\mathrm{MndHom}N\right)\to F:{\mathrm{Base}}_M⟶{\mathrm{Base}}_N$$
20	19	adantr	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> F : ( Base ` M ) --> ( Base ` N ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> F : ( Base ` M ) --> ( Base ` N ) ) with typecode |-
21	20	ffnd	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> F Fn ( Base ` M ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> F Fn ( Base ` M ) ) with typecode |-
22	21	adantr	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> F Fn ( Base ` M ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> F Fn ( Base ` M ) ) with typecode |-
23		eqid	$$⊢{\cdot }_R={\cdot }_R$$
24	1 23	mgpplusg	$$⊢{\cdot }_R={+}_M$$
25	24	eqcomi	$$⊢{+}_M={\cdot }_R$$
26	25	subrngmcl	Could not format ( ( X e. ( SubRng ` R ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X ) : No typesetting found for |- ( ( X e. ( SubRng ` R ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X ) with typecode |-
27	26	3expb	Could not format ( ( X e. ( SubRng ` R ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X ) : No typesetting found for |- ( ( X e. ( SubRng ` R ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X ) with typecode |-
28	27	adantll	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X ) with typecode |-
29		fnfvima	$$⊢\left(FFn{\mathrm{Base}}_M\wedge X\subseteq {\mathrm{Base}}_M\wedge z{+}_{M}x\in X\right)\to F\left(z{+}_{M}x\right)\in F\left[X\right]$$
30	22 8 28 29	syl3anc	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) ) with typecode |-
31	17 30	eqeltrrd	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) with typecode |-
32	31	anassrs	Could not format ( ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) /\ x e. X ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) : No typesetting found for |- ( ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) /\ x e. X ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) with typecode |-
33	32	ralrimiva	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) with typecode |-
34		oveq2	$$⊢y=F\left(x\right)\to F\left(z\right){+}_{N}y=F\left(z\right){+}_{N}F\left(x\right)$$
35	34	eleq1d	$$⊢y=F\left(x\right)\to \left(F\left(z\right){+}_{N}y\in F\left[X\right]\leftrightarrow F\left(z\right){+}_{N}F\left(x\right)\in F\left[X\right]\right)$$
36	35	ralima	$$⊢\left(FFn{\mathrm{Base}}_M\wedge X\subseteq {\mathrm{Base}}_M\right)\to \left(\forall y\in F\left[X\right]F\left(z\right){+}_{N}y\in F\left[X\right]\leftrightarrow \forall x\in XF\left(z\right){+}_{N}F\left(x\right)\in F\left[X\right]\right)$$
37	21 7 36	syl2anc	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) ) with typecode |-
38	37	adantr	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) ) with typecode |-
39	33 38	mpbird	Could not format ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) : No typesetting found for |- ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) with typecode |-
40	39	ralrimiva	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) with typecode |-
41		oveq1	$$⊢x=F\left(z\right)\to x{+}_{N}y=F\left(z\right){+}_{N}y$$
42	41	eleq1d	$$⊢x=F\left(z\right)\to \left(x{+}_{N}y\in F\left[X\right]\leftrightarrow F\left(z\right){+}_{N}y\in F\left[X\right]\right)$$
43	42	ralbidv	$$⊢x=F\left(z\right)\to \left(\forall y\in F\left[X\right]x{+}_{N}y\in F\left[X\right]\leftrightarrow \forall y\in F\left[X\right]F\left(z\right){+}_{N}y\in F\left[X\right]\right)$$
44	43	ralima	$$⊢\left(FFn{\mathrm{Base}}_M\wedge X\subseteq {\mathrm{Base}}_M\right)\to \left(\forall x\in F\left[X\right]\forall y\in F\left[X\right]x{+}_{N}y\in F\left[X\right]\leftrightarrow \forall z\in X\forall y\in F\left[X\right]F\left(z\right){+}_{N}y\in F\left[X\right]\right)$$
45	21 7 44	syl2anc	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> ( A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> ( A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) ) with typecode |-
46	40 45	mpbird	Could not format ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) : No typesetting found for |- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) with typecode |-