Theorem mhmlem

Description: Lemma for mhmmnd and ghmgrp . (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 25-Jan-2020)

	Ref	Expression
Hypotheses	ghmgrp.f	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
	mhmlem.a	$$⊢\phi \to A\in X$$
	mhmlem.b	$$⊢\phi \to B\in X$$
Assertion	mhmlem	$$⊢\phi \to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ghmgrp.f	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
2		mhmlem.a	$$⊢\phi \to A\in X$$
3		mhmlem.b	$$⊢\phi \to B\in X$$
4		id	$$⊢\phi \to \phi$$
5		eleq1	$$⊢x=A\to \left(x\in X\leftrightarrow A\in X\right)$$
6	5	3anbi2d	$$⊢x=A\to \left(\left(\phi \wedge x\in X\wedge y\in X\right)\leftrightarrow \left(\phi \wedge A\in X\wedge y\in X\right)\right)$$
7		fvoveq1	$$⊢x=A\to F\left(x\underset{\dot{}}{+}y\right)=F\left(A\underset{\dot{}}{+}y\right)$$
8		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
9	8	oveq1d	$$⊢x=A\to F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(y\right)$$
10	7 9	eqeq12d	$$⊢x=A\to \left(F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\leftrightarrow F\left(A\underset{\dot{}}{+}y\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(y\right)\right)$$
11	6 10	imbi12d	$$⊢x=A\to \left(\left(\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\right)\leftrightarrow \left(\left(\phi \wedge A\in X\wedge y\in X\right)\to F\left(A\underset{\dot{}}{+}y\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(y\right)\right)\right)$$
12		eleq1	$$⊢y=B\to \left(y\in X\leftrightarrow B\in X\right)$$
13	12	3anbi3d	$$⊢y=B\to \left(\left(\phi \wedge A\in X\wedge y\in X\right)\leftrightarrow \left(\phi \wedge A\in X\wedge B\in X\right)\right)$$
14		oveq2	$$⊢y=B\to A\underset{\dot{}}{+}y=A\underset{\dot{}}{+}B$$
15	14	fveq2d	$$⊢y=B\to F\left(A\underset{\dot{}}{+}y\right)=F\left(A\underset{\dot{}}{+}B\right)$$
16		fveq2	$$⊢y=B\to F\left(y\right)=F\left(B\right)$$
17	16	oveq2d	$$⊢y=B\to F\left(A\right)\underset{\dot{}}{⨣}F\left(y\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)$$
18	15 17	eqeq12d	$$⊢y=B\to \left(F\left(A\underset{\dot{}}{+}y\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(y\right)\leftrightarrow F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)\right)$$
19	13 18	imbi12d	$$⊢y=B\to \left(\left(\left(\phi \wedge A\in X\wedge y\in X\right)\to F\left(A\underset{\dot{}}{+}y\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(y\right)\right)\leftrightarrow \left(\left(\phi \wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)\right)\right)$$
20	11 19 1	vtocl2g	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\left(\phi \wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)\right)$$
21	2 3 20	syl2anc	$$⊢\phi \to \left(\left(\phi \wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)\right)$$
22	4 2 3 21	mp3and	$$⊢\phi \to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)$$