Theorem mndodconglem

Description: Lemma for mndodcong . (Contributed by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	$$⊢X={\mathrm{Base}}_G$$
	odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
	odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
	mndodconglem.1	$$⊢\phi \to G\in \mathrm{Mnd}$$
	mndodconglem.2	$$⊢\phi \to A\in X$$
	mndodconglem.3	$$⊢\phi \to O\left(A\right)\in \mathbb{N}$$
	mndodconglem.4	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	mndodconglem.5	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mndodconglem.6	$$⊢\phi \to M<O\left(A\right)$$
	mndodconglem.7	$$⊢\phi \to N<O\left(A\right)$$
	mndodconglem.8	$$⊢\phi \to M\underset{\dot{}}{·}A=N\underset{\dot{}}{·}A$$
Assertion	mndodconglem	$$⊢\left(\phi \wedge M\le N\right)\to M=N$$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5		mndodconglem.1	$$⊢\phi \to G\in \mathrm{Mnd}$$
6		mndodconglem.2	$$⊢\phi \to A\in X$$
7		mndodconglem.3	$$⊢\phi \to O\left(A\right)\in \mathbb{N}$$
8		mndodconglem.4	$$⊢\phi \to M\in {\mathbb{N}}_0$$
9		mndodconglem.5	$$⊢\phi \to N\in {\mathbb{N}}_0$$
10		mndodconglem.6	$$⊢\phi \to M<O\left(A\right)$$
11		mndodconglem.7	$$⊢\phi \to N<O\left(A\right)$$
12		mndodconglem.8	$$⊢\phi \to M\underset{\dot{}}{·}A=N\underset{\dot{}}{·}A$$
13	7	nnred	$$⊢\phi \to O\left(A\right)\in ℝ$$
14	13	recnd	$$⊢\phi \to O\left(A\right)\in ℂ$$
15	8	nn0red	$$⊢\phi \to M\in ℝ$$
16	15	recnd	$$⊢\phi \to M\in ℂ$$
17	9	nn0red	$$⊢\phi \to N\in ℝ$$
18	17	recnd	$$⊢\phi \to N\in ℂ$$
19	14 16 18	addsubassd	$$⊢\phi \to O\left(A\right)+M-N=O\left(A\right)+M-N$$
20	7	nnzd	$$⊢\phi \to O\left(A\right)\in \mathbb{Z}$$
21	8	nn0zd	$$⊢\phi \to M\in \mathbb{Z}$$
22	20 21	zaddcld	$$⊢\phi \to O\left(A\right)+M\in \mathbb{Z}$$
23	22	zred	$$⊢\phi \to O\left(A\right)+M\in ℝ$$
24		nn0addge1	$$⊢\left(O\left(A\right)\in ℝ\wedge M\in {\mathbb{N}}_0\right)\to O\left(A\right)\le O\left(A\right)+M$$
25	13 8 24	syl2anc	$$⊢\phi \to O\left(A\right)\le O\left(A\right)+M$$
26	17 13 23 11 25	ltletrd	$$⊢\phi \to N<O\left(A\right)+M$$
27	9	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
28		znnsub	$$⊢\left(N\in \mathbb{Z}\wedge O\left(A\right)+M\in \mathbb{Z}\right)\to \left(N<O\left(A\right)+M\leftrightarrow O\left(A\right)+M-N\in \mathbb{N}\right)$$
29	27 22 28	syl2anc	$$⊢\phi \to \left(N<O\left(A\right)+M\leftrightarrow O\left(A\right)+M-N\in \mathbb{N}\right)$$
30	26 29	mpbid	$$⊢\phi \to O\left(A\right)+M-N\in \mathbb{N}$$
31	19 30	eqeltrrd	$$⊢\phi \to O\left(A\right)+M-N\in \mathbb{N}$$
32	14 16 18	addsub12d	$$⊢\phi \to O\left(A\right)+M-N=M+O\left(A\right)-N$$
33	32	oveq1d	$$⊢\phi \to \left(O\left(A\right)+M-N\right)\underset{\dot{}}{·}A=\left(M+O\left(A\right)-N\right)\underset{\dot{}}{·}A$$
34	12	oveq1d	$$⊢\phi \to \left(M\underset{\dot{}}{·}A\right){+}_G\left(\left(O\left(A\right)-N\right)\underset{\dot{}}{·}A\right)=\left(N\underset{\dot{}}{·}A\right){+}_G\left(\left(O\left(A\right)-N\right)\underset{\dot{}}{·}A\right)$$
35		znnsub	$$⊢\left(N\in \mathbb{Z}\wedge O\left(A\right)\in \mathbb{Z}\right)\to \left(N<O\left(A\right)\leftrightarrow O\left(A\right)-N\in \mathbb{N}\right)$$
36	27 20 35	syl2anc	$$⊢\phi \to \left(N<O\left(A\right)\leftrightarrow O\left(A\right)-N\in \mathbb{N}\right)$$
37	11 36	mpbid	$$⊢\phi \to O\left(A\right)-N\in \mathbb{N}$$
38	37	nnnn0d	$$⊢\phi \to O\left(A\right)-N\in {\mathbb{N}}_0$$
39		eqid	$$⊢{+}_G={+}_G$$
40	1 3 39	mulgnn0dir	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(M\in {\mathbb{N}}_0\wedge O\left(A\right)-N\in {\mathbb{N}}_0\wedge A\in X\right)\right)\to \left(M+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\left(M\underset{\dot{}}{·}A\right){+}_G\left(\left(O\left(A\right)-N\right)\underset{\dot{}}{·}A\right)$$
41	5 8 38 6 40	syl13anc	$$⊢\phi \to \left(M+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\left(M\underset{\dot{}}{·}A\right){+}_G\left(\left(O\left(A\right)-N\right)\underset{\dot{}}{·}A\right)$$
42	1 3 39	mulgnn0dir	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(N\in {\mathbb{N}}_0\wedge O\left(A\right)-N\in {\mathbb{N}}_0\wedge A\in X\right)\right)\to \left(N+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\left(N\underset{\dot{}}{·}A\right){+}_G\left(\left(O\left(A\right)-N\right)\underset{\dot{}}{·}A\right)$$
43	5 9 38 6 42	syl13anc	$$⊢\phi \to \left(N+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\left(N\underset{\dot{}}{·}A\right){+}_G\left(\left(O\left(A\right)-N\right)\underset{\dot{}}{·}A\right)$$
44	34 41 43	3eqtr4d	$$⊢\phi \to \left(M+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\left(N+O\left(A\right)-N\right)\underset{\dot{}}{·}A$$
45	18 14	pncan3d	$$⊢\phi \to N+O\left(A\right)-N=O\left(A\right)$$
46	45	oveq1d	$$⊢\phi \to \left(N+O\left(A\right)-N\right)\underset{\dot{}}{·}A=O\left(A\right)\underset{\dot{}}{·}A$$
47	1 2 3 4	odid	$$⊢A\in X\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
48	6 47	syl	$$⊢\phi \to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
49	46 48	eqtrd	$$⊢\phi \to \left(N+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
50	44 49	eqtrd	$$⊢\phi \to \left(M+O\left(A\right)-N\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
51	33 50	eqtrd	$$⊢\phi \to \left(O\left(A\right)+M-N\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
52	1 2 3 4	odlem2	$$⊢\left(A\in X\wedge O\left(A\right)+M-N\in \mathbb{N}\wedge \left(O\left(A\right)+M-N\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\to O\left(A\right)\in \left(1\dots O\left(A\right)+M-N\right)$$
53	6 31 51 52	syl3anc	$$⊢\phi \to O\left(A\right)\in \left(1\dots O\left(A\right)+M-N\right)$$
54		elfzle2	$$⊢O\left(A\right)\in \left(1\dots O\left(A\right)+M-N\right)\to O\left(A\right)\le O\left(A\right)+M-N$$
55	53 54	syl	$$⊢\phi \to O\left(A\right)\le O\left(A\right)+M-N$$
56	21 27	zsubcld	$$⊢\phi \to M-N\in \mathbb{Z}$$
57	56	zred	$$⊢\phi \to M-N\in ℝ$$
58	13 57	addge01d	$$⊢\phi \to \left(0\le M-N\leftrightarrow O\left(A\right)\le O\left(A\right)+M-N\right)$$
59	55 58	mpbird	$$⊢\phi \to 0\le M-N$$
60	15 17	subge0d	$$⊢\phi \to \left(0\le M-N\leftrightarrow N\le M\right)$$
61	59 60	mpbid	$$⊢\phi \to N\le M$$
62	15 17	letri3d	$$⊢\phi \to \left(M=N\leftrightarrow \left(M\le N\wedge N\le M\right)\right)$$
63	62	biimprd	$$⊢\phi \to \left(\left(M\le N\wedge N\le M\right)\to M=N\right)$$
64	61 63	mpan2d	$$⊢\phi \to \left(M\le N\to M=N\right)$$
65	64	imp	$$⊢\left(\phi \wedge M\le N\right)\to M=N$$