Theorem mhmimalem

Description: Lemma for mhmima and similar theorems, formerly part of proof for mhmima . (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by AV, 16-Feb-2025)

	Ref	Expression
Hypotheses	mhmimalem.f	$$⊢\phi \to F\in \left(M\mathrm{MndHom}N\right)$$
	mhmimalem.s	$$⊢\phi \to X\subseteq {\mathrm{Base}}_M$$
	mhmimalem.a	$$⊢\phi \to \underset{\dot{}}{\oplus }={+}_M$$
	mhmimalem.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_N$$
	mhmimalem.c	$$⊢\left(\phi \wedge z\in X\wedge x\in X\right)\to z\underset{\dot{}}{\oplus }x\in X$$
Assertion	mhmimalem	$$⊢\phi \to \forall x\in F\left[X\right]\forall y\in F\left[X\right]x\underset{\dot{}}{+}y\in F\left[X\right]$$

Proof

Step	Hyp	Ref	Expression
1		mhmimalem.f	$$⊢\phi \to F\in \left(M\mathrm{MndHom}N\right)$$
2		mhmimalem.s	$$⊢\phi \to X\subseteq {\mathrm{Base}}_M$$
3		mhmimalem.a	$$⊢\phi \to \underset{\dot{}}{\oplus }={+}_M$$
4		mhmimalem.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_N$$
5		mhmimalem.c	$$⊢\left(\phi \wedge z\in X\wedge x\in X\right)\to z\underset{\dot{}}{\oplus }x\in X$$
6	1	adantr	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to F\in \left(M\mathrm{MndHom}N\right)$$
7	2	adantr	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to X\subseteq {\mathrm{Base}}_M$$
8		simprl	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to z\in X$$
9	7 8	sseldd	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to z\in {\mathrm{Base}}_M$$
10		simprr	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to x\in X$$
11	7 10	sseldd	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to x\in {\mathrm{Base}}_M$$
12		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
13		eqid	$$⊢{+}_M={+}_M$$
14		eqid	$$⊢{+}_N={+}_N$$
15	12 13 14	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)$$
16	6 9 11 15	syl3anc	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to F\left(z{+}_{M}x\right)=F\left(z\right){+}_{N}F\left(x\right)$$
17	3	oveqd	$$⊢\phi \to z\underset{\dot{}}{\oplus }x=z{+}_{M}x$$
18	17	fveq2d	$$⊢\phi \to F\left(z\underset{\dot{}}{\oplus }x\right)=F\left(z{+}_{M}x\right)$$
19	4	oveqd	$$⊢\phi \to F\left(z\right)\underset{\dot{}}{+}F\left(x\right)=F\left(z\right){+}_{N}F\left(x\right)$$
20	18 19	eqeq12d	$$⊢\phi \to \left(F\left(z\underset{\dot{}}{\oplus }x\right)=F\left(z\right)\underset{\dot{}}{+}F\left(x\right)\leftrightarrow F\left(z{+}_{M}x\right)=F\left(z\right){+}_{N}F\left(x\right)\right)$$
21	20	adantr	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to \left(F\left(z\underset{\dot{}}{\oplus }x\right)=F\left(z\right)\underset{\dot{}}{+}F\left(x\right)\leftrightarrow F\left(z{+}_{M}x\right)=F\left(z\right){+}_{N}F\left(x\right)\right)$$
22	16 21	mpbird	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to F\left(z\underset{\dot{}}{\oplus }x\right)=F\left(z\right)\underset{\dot{}}{+}F\left(x\right)$$
23		eqid	$$⊢{\mathrm{Base}}_N={\mathrm{Base}}_N$$
24	12 23	mhmf	$$⊢F\in \left(M\mathrm{MndHom}N\right)\to F:{\mathrm{Base}}_M⟶{\mathrm{Base}}_N$$
25	1 24	syl	$$⊢\phi \to F:{\mathrm{Base}}_M⟶{\mathrm{Base}}_N$$
26	25	ffnd	$$⊢\phi \to FFn{\mathrm{Base}}_M$$
27	26	adantr	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to FFn{\mathrm{Base}}_M$$
28	5	3expb	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to z\underset{\dot{}}{\oplus }x\in X$$
29		fnfvima	$$⊢\left(FFn{\mathrm{Base}}_M\wedge X\subseteq {\mathrm{Base}}_M\wedge z\underset{\dot{}}{\oplus }x\in X\right)\to F\left(z\underset{\dot{}}{\oplus }x\right)\in F\left[X\right]$$
30	27 7 28 29	syl3anc	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to F\left(z\underset{\dot{}}{\oplus }x\right)\in F\left[X\right]$$
31	22 30	eqeltrrd	$$⊢\left(\phi \wedge \left(z\in X\wedge x\in X\right)\right)\to F\left(z\right)\underset{\dot{}}{+}F\left(x\right)\in F\left[X\right]$$
32	31	anassrs	$$⊢\left(\left(\phi \wedge z\in X\right)\wedge x\in X\right)\to F\left(z\right)\underset{\dot{}}{+}F\left(x\right)\in F\left[X\right]$$
33	32	ralrimiva	$$⊢\left(\phi \wedge z\in X\right)\to \forall x\in XF\left(z\right)\underset{\dot{}}{+}F\left(x\right)\in F\left[X\right]$$
34		oveq2	$$⊢y=F\left(x\right)\to F\left(z\right)\underset{\dot{}}{+}y=F\left(z\right)\underset{\dot{}}{+}F\left(x\right)$$
35	34	eleq1d	$$⊢y=F\left(x\right)\to \left(F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow F\left(z\right)\underset{\dot{}}{+}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)\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow \forall x\in XF\left(z\right)\underset{\dot{}}{+}F\left(x\right)\in F\left[X\right]\right)$$
37	26 2 36	syl2anc	$$⊢\phi \to \left(\forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow \forall x\in XF\left(z\right)\underset{\dot{}}{+}F\left(x\right)\in F\left[X\right]\right)$$
38	37	adantr	$$⊢\left(\phi \wedge z\in X\right)\to \left(\forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow \forall x\in XF\left(z\right)\underset{\dot{}}{+}F\left(x\right)\in F\left[X\right]\right)$$
39	33 38	mpbird	$$⊢\left(\phi \wedge z\in X\right)\to \forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]$$
40	39	ralrimiva	$$⊢\phi \to \forall z\in X\forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]$$
41		oveq1	$$⊢x=F\left(z\right)\to x\underset{\dot{}}{+}y=F\left(z\right)\underset{\dot{}}{+}y$$
42	41	eleq1d	$$⊢x=F\left(z\right)\to \left(x\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow F\left(z\right)\underset{\dot{}}{+}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\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow \forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}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\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow \forall z\in X\forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]\right)$$
45	26 2 44	syl2anc	$$⊢\phi \to \left(\forall x\in F\left[X\right]\forall y\in F\left[X\right]x\underset{\dot{}}{+}y\in F\left[X\right]\leftrightarrow \forall z\in X\forall y\in F\left[X\right]F\left(z\right)\underset{\dot{}}{+}y\in F\left[X\right]\right)$$
46	40 45	mpbird	$$⊢\phi \to \forall x\in F\left[X\right]\forall y\in F\left[X\right]x\underset{\dot{}}{+}y\in F\left[X\right]$$