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	$⊢ φ \to F \in (M MndHom N)$
	mhmimalem.s	$⊢ φ \to X \subseteq {Base}_{M}$
	mhmimalem.a	$⊢ φ \to \underset{˙}{\oplus} = +_{M}$
	mhmimalem.p	$⊢ φ \to \underset{˙}{+} = +_{N}$
	mhmimalem.c	$⊢ (φ \land z \in X \land x \in X) \to z \underset{˙}{\oplus} x \in X$
Assertion	mhmimalem	$⊢ φ \to \forall x \in F [X] \forall y \in F [X] x \underset{˙}{+} y \in F [X]$

Proof

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

Metamath Proof Explorer

Theorem mhmimalem

Proof