Metamath Proof Explorer

Theorem mndodconglem

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

Ref Expression
Hypotheses odcl.1 
|- X = ( Base ` G )
odcl.2 
|- O = ( od ` G )
odid.3 
|- .x. = ( .g ` G )
odid.4 
|- .0. = ( 0g ` G )
mndodconglem.1 
|- ( ph -> G e. Mnd )
mndodconglem.2 
|- ( ph -> A e. X )
mndodconglem.3 
|- ( ph -> ( O ` A ) e. NN )
mndodconglem.4 
|- ( ph -> M e. NN0 )
mndodconglem.5 
|- ( ph -> N e. NN0 )
mndodconglem.6 
|- ( ph -> M < ( O ` A ) )
mndodconglem.7 
|- ( ph -> N < ( O ` A ) )
mndodconglem.8 
|- ( ph -> ( M .x. A ) = ( N .x. A ) )
Assertion mndodconglem 
|- ( ( ph /\ M <_ N ) -> M = N )

Proof

Step Hyp Ref Expression
1 odcl.1 
 |-  X = ( Base ` G )
2 odcl.2 
 |-  O = ( od ` G )
3 odid.3 
 |-  .x. = ( .g ` G )
4 odid.4 
 |-  .0. = ( 0g ` G )
5 mndodconglem.1 
 |-  ( ph -> G e. Mnd )
6 mndodconglem.2 
 |-  ( ph -> A e. X )
7 mndodconglem.3 
 |-  ( ph -> ( O ` A ) e. NN )
8 mndodconglem.4 
 |-  ( ph -> M e. NN0 )
9 mndodconglem.5 
 |-  ( ph -> N e. NN0 )
10 mndodconglem.6 
 |-  ( ph -> M < ( O ` A ) )
11 mndodconglem.7 
 |-  ( ph -> N < ( O ` A ) )
12 mndodconglem.8 
 |-  ( ph -> ( M .x. A ) = ( N .x. A ) )
13 7 nnred 
 |-  ( ph -> ( O ` A ) e. RR )
14 13 recnd 
 |-  ( ph -> ( O ` A ) e. CC )
15 8 nn0red 
 |-  ( ph -> M e. RR )
16 15 recnd 
 |-  ( ph -> M e. CC )
17 9 nn0red 
 |-  ( ph -> N e. RR )
18 17 recnd 
 |-  ( ph -> N e. CC )
19 14 16 18 addsubassd 
 |-  ( ph -> ( ( ( O ` A ) + M ) - N ) = ( ( O ` A ) + ( M - N ) ) )
20 7 nnzd 
 |-  ( ph -> ( O ` A ) e. ZZ )
21 8 nn0zd 
 |-  ( ph -> M e. ZZ )
22 20 21 zaddcld 
 |-  ( ph -> ( ( O ` A ) + M ) e. ZZ )
23 22 zred 
 |-  ( ph -> ( ( O ` A ) + M ) e. RR )
24 nn0addge1 
 |-  ( ( ( O ` A ) e. RR /\ M e. NN0 ) -> ( O ` A ) <_ ( ( O ` A ) + M ) )
25 13 8 24 syl2anc 
 |-  ( ph -> ( O ` A ) <_ ( ( O ` A ) + M ) )
26 17 13 23 11 25 ltletrd 
 |-  ( ph -> N < ( ( O ` A ) + M ) )
27 9 nn0zd 
 |-  ( ph -> N e. ZZ )
28 znnsub 
 |-  ( ( N e. ZZ /\ ( ( O ` A ) + M ) e. ZZ ) -> ( N < ( ( O ` A ) + M ) <-> ( ( ( O ` A ) + M ) - N ) e. NN ) )
29 27 22 28 syl2anc 
 |-  ( ph -> ( N < ( ( O ` A ) + M ) <-> ( ( ( O ` A ) + M ) - N ) e. NN ) )
30 26 29 mpbid 
 |-  ( ph -> ( ( ( O ` A ) + M ) - N ) e. NN )
31 19 30 eqeltrrd 
 |-  ( ph -> ( ( O ` A ) + ( M - N ) ) e. NN )
32 14 16 18 addsub12d 
 |-  ( ph -> ( ( O ` A ) + ( M - N ) ) = ( M + ( ( O ` A ) - N ) ) )
33 32 oveq1d 
 |-  ( ph -> ( ( ( O ` A ) + ( M - N ) ) .x. A ) = ( ( M + ( ( O ` A ) - N ) ) .x. A ) )
34 12 oveq1d 
 |-  ( ph -> ( ( M .x. A ) ( +g ` G ) ( ( ( O ` A ) - N ) .x. A ) ) = ( ( N .x. A ) ( +g ` G ) ( ( ( O ` A ) - N ) .x. A ) ) )
35 znnsub 
 |-  ( ( N e. ZZ /\ ( O ` A ) e. ZZ ) -> ( N < ( O ` A ) <-> ( ( O ` A ) - N ) e. NN ) )
36 27 20 35 syl2anc 
 |-  ( ph -> ( N < ( O ` A ) <-> ( ( O ` A ) - N ) e. NN ) )
37 11 36 mpbid 
 |-  ( ph -> ( ( O ` A ) - N ) e. NN )
38 37 nnnn0d 
 |-  ( ph -> ( ( O ` A ) - N ) e. NN0 )
39 eqid 
 |-  ( +g ` G ) = ( +g ` G )
40 1 3 39 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ ( ( O ` A ) - N ) e. NN0 /\ A e. X ) ) -> ( ( M + ( ( O ` A ) - N ) ) .x. A ) = ( ( M .x. A ) ( +g ` G ) ( ( ( O ` A ) - N ) .x. A ) ) )
41 5 8 38 6 40 syl13anc 
 |-  ( ph -> ( ( M + ( ( O ` A ) - N ) ) .x. A ) = ( ( M .x. A ) ( +g ` G ) ( ( ( O ` A ) - N ) .x. A ) ) )
42 1 3 39 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( N e. NN0 /\ ( ( O ` A ) - N ) e. NN0 /\ A e. X ) ) -> ( ( N + ( ( O ` A ) - N ) ) .x. A ) = ( ( N .x. A ) ( +g ` G ) ( ( ( O ` A ) - N ) .x. A ) ) )
43 5 9 38 6 42 syl13anc 
 |-  ( ph -> ( ( N + ( ( O ` A ) - N ) ) .x. A ) = ( ( N .x. A ) ( +g ` G ) ( ( ( O ` A ) - N ) .x. A ) ) )
44 34 41 43 3eqtr4d 
 |-  ( ph -> ( ( M + ( ( O ` A ) - N ) ) .x. A ) = ( ( N + ( ( O ` A ) - N ) ) .x. A ) )
45 18 14 pncan3d 
 |-  ( ph -> ( N + ( ( O ` A ) - N ) ) = ( O ` A ) )
46 45 oveq1d 
 |-  ( ph -> ( ( N + ( ( O ` A ) - N ) ) .x. A ) = ( ( O ` A ) .x. A ) )
47 1 2 3 4 odid 
 |-  ( A e. X -> ( ( O ` A ) .x. A ) = .0. )
48 6 47 syl 
 |-  ( ph -> ( ( O ` A ) .x. A ) = .0. )
49 46 48 eqtrd 
 |-  ( ph -> ( ( N + ( ( O ` A ) - N ) ) .x. A ) = .0. )
50 44 49 eqtrd 
 |-  ( ph -> ( ( M + ( ( O ` A ) - N ) ) .x. A ) = .0. )
51 33 50 eqtrd 
 |-  ( ph -> ( ( ( O ` A ) + ( M - N ) ) .x. A ) = .0. )
52 1 2 3 4 odlem2 
 |-  ( ( A e. X /\ ( ( O ` A ) + ( M - N ) ) e. NN /\ ( ( ( O ` A ) + ( M - N ) ) .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... ( ( O ` A ) + ( M - N ) ) ) )
53 6 31 51 52 syl3anc 
 |-  ( ph -> ( O ` A ) e. ( 1 ... ( ( O ` A ) + ( M - N ) ) ) )
54 elfzle2 
 |-  ( ( O ` A ) e. ( 1 ... ( ( O ` A ) + ( M - N ) ) ) -> ( O ` A ) <_ ( ( O ` A ) + ( M - N ) ) )
55 53 54 syl 
 |-  ( ph -> ( O ` A ) <_ ( ( O ` A ) + ( M - N ) ) )
56 21 27 zsubcld 
 |-  ( ph -> ( M - N ) e. ZZ )
57 56 zred 
 |-  ( ph -> ( M - N ) e. RR )
58 13 57 addge01d 
 |-  ( ph -> ( 0 <_ ( M - N ) <-> ( O ` A ) <_ ( ( O ` A ) + ( M - N ) ) ) )
59 55 58 mpbird 
 |-  ( ph -> 0 <_ ( M - N ) )
60 15 17 subge0d 
 |-  ( ph -> ( 0 <_ ( M - N ) <-> N <_ M ) )
61 59 60 mpbid 
 |-  ( ph -> N <_ M )
62 15 17 letri3d 
 |-  ( ph -> ( M = N <-> ( M <_ N /\ N <_ M ) ) )
63 62 biimprd 
 |-  ( ph -> ( ( M <_ N /\ N <_ M ) -> M = N ) )
64 61 63 mpan2d 
 |-  ( ph -> ( M <_ N -> M = N ) )
65 64 imp 
 |-  ( ( ph /\ M <_ N ) -> M = N )